Theorem nfcv 2319

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 1528	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
2	1	nfci 2309	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:   ∈ wcel 2148  Ⅎwnfc 2306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1449  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-nfc 2308

This theorem is referenced by:  nfcvd  2320  nfel  2328  nfeq1  2329  nfel1  2330  nfeq2  2331  nfel2  2332  nfcvf  2342  r2al  2496  r2ex  2497  nfraldxy  2510  nfrexdxy  2511  nfra2xy  2519  r19.12  2583  ralcom  2640  rexcom  2641  nfreudxy  2650  raleq  2672  rexeq  2673  reueq1  2674  rmoeq1  2675  cbvralw  2698  cbvral  2699  cbvrex  2700  rabeq  2729  rabeqi  2730  cbvrabv  2736  vtoclg  2797  vtocl2g  2801  vtoclga  2803  vtocl2ga  2805  vtocl3ga  2807  spcimdv  2821  spcimedv  2823  spcgv  2824  spcegv  2825  rspct  2834  rspc  2835  rspce  2836  rspc2  2852  ceqsexg  2865  elabgt  2878  elabf  2880  elabg  2883  elab3g  2888  elrab  2893  mob  2919  nfsbc1v  2981  elrabsf  3001  sbcralt  3039  sbcrext  3040  sbcralg  3041  sbcrex  3042  sbcreug  3043  cbvcsbv  3063  csbconstg  3071  nfcsb1v  3090  csbie  3102  csbnestg  3111  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  cbvralv2  3123  cbvrexv2  3124  dfss4st  3368  n0rf  3435  n0r  3436  eq0  3441  raaanlem  3528  nfpw  3588  cbviunv  3925  cbviinv  3926  ssiun2s  3930  iunab  3933  ssiinf  3936  ssiin  3937  iinab  3948  cbvdisjv  3991  nfdisjv  3992  disjnims  3995  disji2  3996  cbvmptv  4099  triun  4114  csbexga  4131  repizf2  4162  moop2  4251  euotd  4254  opelopabf  4274  nfpo  4301  nfso  4302  pofun  4312  nfse  4341  nffrfor  4348  nffr  4349  frind  4352  nfwe  4355  eusvnf  4453  rabxfrd  4469  tfis  4582  tfisi  4586  opeliunxp  4681  nfrel  4711  opeliunxp2  4767  ralxpf  4773  rexxpf  4774  nfco  4792  nfcnv  4806  dfdmf  4820  dfrnf  4868  nfdm  4871  nfres  4909  resmptf  4957  nfiotadw  5181  dffun6f  5229  dffun6  5230  dffun4f  5232  nffun  5239  funimaexglem  5299  nffv  5525  nffvmpt1  5526  dffn5imf  5571  funfvdm2f  5581  fvmptss2  5591  fvmpts  5594  fvmpt2  5599  fvmptssdm  5600  mptfvex  5601  fvmptdv  5604  fvmptd3  5609  elfvmptrab1  5610  eqfnfv2f  5617  ralrnmpt  5658  rexrnmpt  5659  f1ompt  5667  ffnfvf  5675  fmptco  5682  fmptcof  5683  fmptcos  5684  funiunfvdmf  5764  dff13f  5770  f1mpt  5771  fliftfuns  5798  nfiso  5806  nfriotadxy  5838  csbriotag  5842  riota2  5852  mpoeq123  5933  cbvmpox  5952  cbvmpo  5953  cbvmpov  5954  ovmpos  5997  ov2gf  5998  ovmpodxf  5999  ovmpodx  6000  ovmpodv  6006  ovmpodv2  6007  ovi3  6010  nfof  6087  nfofr  6088  offval2  6097  ofrfval2  6098  abrexex2g  6120  abrexex2  6124  dfopab2  6189  dfoprab3s  6190  mpomptsx  6197  dmmpossx  6199  fmpox  6200  mpofvex  6203  fnmpoovd  6215  fmpoco  6216  dfmpo  6223  f1od2  6235  disjxp1  6236  mpoxopoveq  6240  mpoxopovel  6241  nftpos  6279  tposoprab  6280  nfrecs  6307  nffrec  6396  eqerlem  6565  qliftfuns  6618  cbvixpv  6715  nfixpxy  6716  nfixp1  6717  ixpf  6719  mptelixpg  6733  dom2lem  6771  xpcomco  6825  xpf1o  6843  mapxpen  6847  ac6sfi  6897  nfsup  6990  nfdju  7040  exmidomni  7139  ismkvnex  7152  cc2  7265  cc4f  7267  cc4  7268  caucvgprprlemaddq  7706  caucvgsrlemgt1  7793  axpre-suploclemres  7899  lble  8903  supinfneg  9594  infsupneg  9595  fzrevral  10104  nfseq  10454  seq3f1olemstep  10500  seq3f1olemp  10501  fimaxre2  11234  nfsum1  11363  nfsum  11364  cbvsumv  11368  cbvsumi  11369  sumfct  11381  sumrbdclem  11384  summodclem2a  11388  zsumdc  11391  fsum3  11394  isumss  11398  isumss2  11400  fsum3cvg2  11401  fsumzcl2  11412  fsumadd  11413  fsumsplitf  11415  sumsnf  11416  sumsn  11418  sumsns  11422  fsumsplitsnun  11426  fsum2dlemstep  11441  fisumcom2  11445  fsumshftm  11452  fsum00  11469  fsumrelem  11478  fsumiun  11484  mertenslem2  11543  prodeq1  11560  nfcprod1  11561  nfcprod  11562  cbvprod  11565  cbvprodv  11566  cbvprodi  11567  prodrbdclem  11578  prodmodclem2a  11583  zproddc  11586  fprodseq  11590  fprodntrivap  11591  prodfct  11594  prodssdc  11596  prodsnf  11599  prodsn  11600  fprodm1s  11608  fprodp1s  11609  prodsns  11610  fprodcllemf  11620  fprodconst  11627  fprodap0  11628  fprod2dlemstep  11629  fprodcom2fi  11633  fprodrec  11636  fproddivapf  11638  fprodsplitf  11639  fprodap0f  11643  fprodle  11647  zsupcllemstep  11945  infssuzex  11949  infssuzcldc  11951  bezoutlemmain  11998  bezout  12011  nnwofdc  12038  nnwosdc  12039  prmind2  12119  oddpwdclemdvds  12169  oddpwdclemndvds  12170  pcmpt  12340  pcmptdvds  12342  ctiunctlemudc  12437  ctiunctlemf  12438  ctiunctlemfo  12439  ctiunct  12440  ctiunctal  12441  cnmpt11  13753  cnmpt1t  13755  cnmpt21  13761  cnmpt2t  13763  cnmptcom  13768  imasnopn  13769  fsumcncntop  14026  ellimc3apf  14099  ellimc3ap  14100  limcmpted  14102  lgseisenlem2  14421  elabf1  14503  elabf2  14504  elabg2  14507  bj-omssind  14657  bj-bdfindisg  14670  bj-nntrans  14673  bj-nnelirr  14675  bj-omtrans  14678  setindis  14689  bdsetindis  14691  bj-nn0sucALT  14700  bj-findis  14701  bj-findisg  14702  strcollnfALT  14708  isomninnlem  14748  trilpolemeq1  14758  trirec0  14762  iswomninnlem  14767  ismkvnnlem  14770  nconstwlpolemgt0  14781