Theorem nfcvd 2900

Description: If 𝑥 is disjoint from 𝐴, then 𝑥 is not free in 𝐴. (Contributed by Mario Carneiro, 7-Oct-2016.)

Assertion

Ref	Expression
nfcvd	⊢ (𝜑 → Ⅎ𝑥𝐴)

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem nfcvd

Step	Hyp	Ref	Expression
1		nfcv 2899	. 2 ⊢ Ⅎ𝑥𝐴
2	1	a1i 11	1 ⊢ (𝜑 → Ⅎ𝑥𝐴)

Syntax hints:   → wi 4  Ⅎwnfc 2879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-ex 1775  df-nf 1779  df-nfc 2881

This theorem is referenced by:  nfeld  2910  nfraldwOLD  3314  ralcom2  3369  nfreuwOLD  3418  nfrmowOLD  3419  issetft  3484  vtocldOLD  3545  sbcralt  3863  sbcrext  3864  csbiedOLD  3929  csbie2t  3931  sbcco3gw  4418  sbcco3g  4423  csbco3g  4424  dfnfc2  4927  nfdisjw  5119  eusvnfb  5387  eusv2i  5388  dfid3  5573  iota2d  6530  iota2  6531  fmptcof  7133  nfriotadw  7378  riotaeqimp  7397  riota5f  7399  riota5  7400  oprabid  7446  opiota  8057  fmpoco  8094  nfttrcld  9727  axrepndlem1  10609  axrepndlem2  10610  axunnd  10613  axpowndlem2  10615  axpowndlem3  10616  axpowndlem4  10617  axpownd  10618  axregndlem2  10620  axinfndlem1  10622  axinfnd  10623  axacndlem4  10627  axacndlem5  10628  axacnd  10629  nfnegd  11479  prodsn  15932  fprodeq0g  15964  bpolylem  16018  pcmpt  16854  chfacfpmmulfsupp  22758  elmptrab  23724  dvfsumrlim3  25961  itgsubstlem  25976  itgsubst  25977  ifeqeqx  32326  disjunsn  32377  bj-elgab  36411  bj-gabima  36412  wl-issetft  37043  unirep  37181  riotasv2d  38423  cdleme31so  39846  cdleme31se  39849  cdleme31sc  39851  cdleme31sde  39852  cdleme31sn2  39856  cdlemeg47rv2  39977  cdlemk41  40387  mapdheq  41195  hdmap1eq  41268  hdmapval2lem  41298  monotuz  42356  oddcomabszz  42359  mnringvald  43639  nfxnegd  44817  fprodsplit1  44975  dvnmul  45325  sge0sn  45761  hoidmvlelem3  45979

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »