Theorem nfcv 2374

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

Syntax hints:   ∈ wcel 2202  Ⅎwnfc 2361

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 1497  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-nfc 2363

This theorem is referenced by:  nfcvd  2375  nfel  2383  nfeq1  2384  nfel1  2385  nfeq2  2386  nfel2  2387  nfcvf  2397  r2al  2551  r2ex  2552  nfraldxy  2565  nfrexdxy  2566  nfra2xy  2574  r19.12  2639  ralcom  2696  rexcom  2697  nfreudxy  2707  raleq  2730  rexeq  2731  reueq1  2732  rmoeq1  2733  cbvralw  2760  cbvrexw  2761  cbvral  2763  cbvrex  2764  rabeq  2794  rabeqi  2795  cbvrabv  2801  vtoclg  2864  vtocl2g  2868  vtoclga  2870  vtocl2ga  2872  vtocl3ga  2874  spcimdv  2890  spcimedv  2892  spcgv  2893  spcegv  2894  rspct  2903  rspc  2904  rspce  2905  rspc2  2921  ceqsexg  2934  elabgt  2947  elabf  2949  elabg  2952  elab3g  2957  elrab  2962  mob  2988  nfsbc1v  3050  elrabsf  3070  sbcralt  3108  sbcrext  3109  sbcralg  3110  sbcrex  3111  sbcreug  3112  reu8nf  3113  cbvcsbv  3133  csbconstg  3141  nfcsb1v  3160  csbie  3173  csbnestg  3182  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  cbvralv2  3194  cbvrexv2  3195  dfss4st  3440  n0rf  3507  n0r  3508  eq0  3513  raaanlem  3599  nfpw  3665  cbviunv  4009  cbviinv  4010  ssiun2s  4014  iunab  4017  ssiinf  4020  ssiin  4021  iinab  4032  cbvdisjv  4075  nfdisjv  4076  disjnims  4079  disji2  4080  invdisjrab  4082  cbvmptv  4185  triun  4200  csbexga  4217  repizf2  4252  moop2  4344  euotd  4347  opelopabgf  4364  opelopabf  4369  nfpo  4398  nfso  4399  pofun  4409  nfse  4438  nffrfor  4445  nffr  4446  frind  4449  nfwe  4452  eusvnf  4550  rabxfrd  4566  tfis  4681  tfisi  4685  opeliunxp  4781  nfrel  4811  opeliunxp2  4870  ralxpf  4876  rexxpf  4877  nfco  4895  nfcnv  4909  dfdmf  4924  dfrnf  4973  nfdm  4976  nfres  5015  resmptf  5063  nfiotadw  5289  dffun6f  5339  dffun6  5340  dffun4f  5342  nffun  5349  funimaexglem  5413  nffv  5649  nffvmpt1  5650  dffn5imf  5701  funfvdm2f  5711  fvmptss2  5721  fvmpts  5724  fvmpt2  5730  fvmptssdm  5731  mptfvex  5732  fvmptdv  5735  fvmptd3  5740  elfvmptrab1  5741  eqfnfv2f  5748  ralrnmpt  5789  rexrnmpt  5790  f1ompt  5798  ffnfvf  5806  fmptco  5813  fmptcof  5814  fmptcos  5815  funiunfvdmf  5905  dff13f  5911  f1mpt  5912  fliftfuns  5939  nfiso  5947  nfriotadxy  5980  csbriotag  5985  riota2  5995  mpoeq123  6080  cbvmpox  6099  cbvmpo  6100  cbvmpov  6101  ovmpos  6145  ov2gf  6146  ovmpodxf  6147  ovmpodx  6148  ovmpodv  6154  ovmpodv2  6155  fvmpopr2d  6158  ovi3  6159  elovmporab  6222  elovmporab1w  6223  nfof  6241  nfofr  6242  offval2  6251  ofrfval2  6252  abrexex2g  6282  abrexex2  6286  uchoice  6300  dfopab2  6352  dfoprab3s  6353  mpomptsx  6362  dmmpossx  6364  fmpox  6365  mpofvex  6370  fnmpoovd  6380  fmpoco  6381  dfmpo  6388  f1od2  6400  disjxp1  6401  mpoxopoveq  6406  mpoxopovel  6407  nftpos  6445  tposoprab  6446  nfrecs  6473  nffrec  6562  eqerlem  6733  qliftfuns  6788  cbvixpv  6885  nfixpxy  6886  nfixp1  6887  ixpf  6889  mptelixpg  6903  dom2lem  6945  modom  6994  xpcomco  7010  xpf1o  7030  mapxpen  7034  ac6sfi  7087  opabfi  7132  nfsup  7191  nfdju  7241  exmidomni  7341  ismkvnex  7354  cc2  7486  cc4f  7488  cc4  7489  caucvgprprlemaddq  7928  caucvgsrlemgt1  8015  axpre-suploclemres  8121  lble  9127  supinfneg  9829  infsupneg  9830  fzrevral  10340  zsupcllemstep  10490  infssuzex  10494  infssuzcldc  10496  nfseq  10720  seq3f1olemstep  10777  seq3f1olemp  10778  nfwrd  11146  reuccatpfxs1v  11333  fimaxre2  11792  nfsum1  11921  nfsum  11922  cbvsumv  11926  cbvsumi  11927  sumfct  11939  sumrbdclem  11943  summodclem2a  11947  zsumdc  11950  fsum3  11953  isumss  11957  isumss2  11959  fsum3cvg2  11960  fsumzcl2  11971  fsumadd  11972  fsumsplitf  11974  sumsnf  11975  sumsn  11977  sumsns  11981  fsumsplitsnun  11985  fsum2dlemstep  12000  fisumcom2  12004  fsumshftm  12011  fsum00  12028  fsumrelem  12037  fsumiun  12043  mertenslem2  12102  prodeq1  12119  nfcprod1  12120  nfcprod  12121  cbvprod  12124  cbvprodv  12125  cbvprodi  12126  prodrbdclem  12137  prodmodclem2a  12142  zproddc  12145  fprodseq  12149  fprodntrivap  12150  prodfct  12153  prodssdc  12155  prodsnf  12158  prodsn  12159  fprodm1s  12167  fprodp1s  12168  prodsns  12169  fprodcllemf  12179  fprodconst  12186  fprodap0  12187  fprod2dlemstep  12188  fprodcom2fi  12192  fprodrec  12195  fproddivapf  12197  fprodsplitf  12198  fprodap0f  12202  fprodle  12206  bezoutlemmain  12574  bezout  12587  nnwofdc  12614  nnwosdc  12615  prmind2  12697  oddpwdclemdvds  12747  oddpwdclemndvds  12748  pcmpt  12921  pcmptdvds  12923  ctiunctlemudc  13063  ctiunctlemf  13064  ctiunctlemfo  13065  ctiunct  13066  ctiunctal  13067  prdsbas3  13375  gsumfzconstf  13934  gsumsplit0  13938  cnmpt11  15013  cnmpt1t  15015  cnmpt21  15021  cnmpt2t  15023  cnmptcom  15028  imasnopn  15029  fsumcncntop  15297  ellimc3apf  15390  ellimc3ap  15391  limcmpted  15393  dvmptfsum  15455  elplyd  15471  fsumdvdsmul  15721  lgseisenlem2  15806  gropd  15904  grstructd2dom  15905  lfgrnloopen  15990  elabf1  16403  elabf2  16404  elabg2  16407  bj-omssind  16556  bj-bdfindisg  16569  bj-nntrans  16572  bj-nnelirr  16574  bj-omtrans  16577  setindis  16588  bdsetindis  16590  bj-nn0sucALT  16599  bj-findis  16600  bj-findisg  16601  strcollnfALT  16607  isomninnlem  16660  trilpolemeq1  16670  trirec0  16674  iswomninnlem  16680  ismkvnnlem  16683  nconstwlpolemgt0  16695  gfsumsn  16712