Theorem nfcv 2281

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

Assertion

Ref	Expression
nfcv	⊢ Ⅎ𝑥𝐴

Distinct variable group:   𝑥,𝐴

Proof of Theorem nfcv

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1508	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
2	1	nfci 2271	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:   ∈ wcel 1480  Ⅎwnfc 2268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1425  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-nfc 2270

This theorem is referenced by:  nfcvd  2282  nfel  2290  nfeq1  2291  nfel1  2292  nfeq2  2293  nfel2  2294  nfcvf  2303  r2al  2454  r2ex  2455  nfraldxy  2467  nfrexdxy  2468  nfra2xy  2475  r19.12  2538  ralcom  2594  rexcom  2595  nfreudxy  2604  raleq  2626  rexeq  2627  reueq1  2628  rmoeq1  2629  cbvral  2650  cbvrex  2651  rabeq  2678  rabeqi  2679  cbvrabv  2685  vtoclg  2746  vtocl2g  2750  vtoclga  2752  vtocl2ga  2754  vtocl3ga  2756  spcimdv  2770  spcimedv  2772  spcgv  2773  spcegv  2774  rspct  2782  rspc  2783  rspce  2784  rspc2  2800  ceqsexg  2813  elabgt  2825  elabf  2827  elabg  2830  elab3g  2835  elrab  2840  mob  2866  nfsbc1v  2927  elrabsf  2947  sbcralt  2985  sbcrext  2986  sbcralg  2987  sbcrex  2988  sbcreug  2989  cbvcsbv  3009  csbconstg  3016  nfcsb1v  3035  csbie  3045  csbnestg  3054  cbvralcsf  3062  cbvrexcsf  3063  cbvreucsf  3064  cbvrabcsf  3065  cbvralv2  3066  cbvrexv2  3067  dfss4st  3309  n0rf  3375  n0r  3376  eq0  3381  raaanlem  3468  nfpw  3523  cbviunv  3852  cbviinv  3853  ssiun2s  3857  iunab  3859  ssiinf  3862  ssiin  3863  iinab  3874  cbvdisjv  3917  nfdisjv  3918  disjnims  3921  disji2  3922  cbvmptv  4024  triun  4039  csbexga  4056  repizf2  4086  moop2  4173  euotd  4176  opelopabf  4196  nfpo  4223  nfso  4224  pofun  4234  nfse  4263  nffrfor  4270  nffr  4271  frind  4274  nfwe  4277  eusvnf  4374  rabxfrd  4390  tfis  4497  tfisi  4501  opeliunxp  4594  nfrel  4624  opeliunxp2  4679  ralxpf  4685  rexxpf  4686  nfco  4704  nfcnv  4718  dfdmf  4732  dfrnf  4780  nfdm  4783  nfres  4821  resmptf  4869  nfiotadw  5091  dffun6f  5136  dffun6  5137  dffun4f  5139  nffun  5146  funimaexglem  5206  nffv  5431  nffvmpt1  5432  dffn5imf  5476  funfvdm2f  5486  fvmptss2  5496  fvmpts  5499  fvmpt2  5504  fvmptssdm  5505  mptfvex  5506  fvmptdv  5509  fvmptd3  5514  elfvmptrab1  5515  eqfnfv2f  5522  ralrnmpt  5562  rexrnmpt  5563  f1ompt  5571  ffnfvf  5579  fmptco  5586  fmptcof  5587  fmptcos  5588  funiunfvdmf  5665  dff13f  5671  f1mpt  5672  fliftfuns  5699  nfiso  5707  nfriotadxy  5738  csbriotag  5742  riota2  5752  mpoeq123  5830  cbvmpox  5849  cbvmpo  5850  cbvmpov  5851  ovmpos  5894  ov2gf  5895  ovmpodxf  5896  ovmpodx  5897  ovmpodv  5903  ovmpodv2  5904  ovi3  5907  nfof  5987  nfofr  5988  offval2  5997  ofrfval2  5998  abrexex2g  6018  abrexex2  6022  dfopab2  6087  dfoprab3s  6088  mpomptsx  6095  dmmpossx  6097  fmpox  6098  mpofvex  6101  fnmpoovd  6112  fmpoco  6113  dfmpo  6120  f1od2  6132  disjxp1  6133  mpoxopoveq  6137  mpoxopovel  6138  nftpos  6176  tposoprab  6177  nfrecs  6204  nffrec  6293  eqerlem  6460  qliftfuns  6513  cbvixpv  6610  nfixpxy  6611  nfixp1  6612  ixpf  6614  mptelixpg  6628  dom2lem  6666  xpcomco  6720  xpf1o  6738  mapxpen  6742  ac6sfi  6792  nfsup  6879  nfdju  6927  exmidomni  7014  ismkvnex  7029  caucvgprprlemaddq  7516  caucvgsrlemgt1  7603  axpre-suploclemres  7709  lble  8705  supinfneg  9390  infsupneg  9391  fzrevral  9885  nfseq  10228  seq3f1olemstep  10274  seq3f1olemp  10275  fimaxre2  10998  nfsum1  11125  nfsum  11126  cbvsumv  11130  cbvsumi  11131  sumfct  11143  sumrbdclem  11146  summodclem2a  11150  zsumdc  11153  fsum3  11156  isumss  11160  isumss2  11162  fsum3cvg2  11163  fsumzcl2  11174  fsumadd  11175  fsumsplitf  11177  sumsnf  11178  sumsn  11180  sumsns  11184  fsumsplitsnun  11188  fsum2dlemstep  11203  fisumcom2  11207  fsumshftm  11214  fsum00  11231  fsumrelem  11240  fsumiun  11246  mertenslem2  11305  prodeq1  11322  nfcprod1  11323  nfcprod  11324  cbvprod  11327  cbvprodv  11328  cbvprodi  11329  prodrbdclem  11340  prodmodclem2a  11345  zsupcllemstep  11638  infssuzex  11642  infssuzcldc  11644  bezoutlemmain  11686  bezout  11699  prmind2  11801  oddpwdclemdvds  11848  oddpwdclemndvds  11849  ctiunctlemudc  11950  ctiunctlemf  11951  ctiunctlemfo  11952  ctiunct  11953  cnmpt11  12452  cnmpt1t  12454  cnmpt21  12460  cnmpt2t  12462  cnmptcom  12467  imasnopn  12468  fsumcncntop  12725  ellimc3apf  12798  ellimc3ap  12799  limcmpted  12801  elabf1  12988  elabf2  12989  elabg2  12992  bj-omssind  13133  bj-bdfindisg  13146  bj-nntrans  13149  bj-nnelirr  13151  bj-omtrans  13154  setindis  13165  bdsetindis  13167  bj-nn0sucALT  13176  bj-findis  13177  bj-findisg  13178  strcollnfALT  13184  isomninnlem  13225  trilpolemeq1  13233