Theorem nfcv 2386

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

Syntax hints:   ∈ wcel 2205  Ⅎwnfc 2373

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 1498  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-nfc 2375

This theorem is referenced by:  nfcvd  2387  nfel  2395  nfeq1  2396  nfel1  2397  nfeq2  2398  nfel2  2399  nfcvf  2409  r2al  2563  r2ex  2564  nfraldxy  2577  nfrexdxy  2578  nfra2xy  2586  r19.12  2651  ralcom  2708  rexcom  2709  nfreudxy  2719  raleq  2743  rexeq  2744  reueq1  2745  rmoeq1  2746  cbvralw  2773  cbvrexw  2774  cbvral  2776  cbvrex  2777  rabeq  2807  rabeqi  2808  cbvrabv  2814  vtoclg  2877  vtocl2g  2881  vtoclga  2883  vtocl2ga  2885  vtocl3ga  2887  spcimdv  2903  spcimedv  2905  spcgv  2906  spcegv  2907  rspct  2916  rspc  2917  rspce  2918  rspc2  2935  ceqsexg  2948  elabgt  2961  elabf  2963  elabg  2966  elab3g  2971  elrab  2976  mob  3002  nfsbc1v  3064  elrabsf  3084  sbcralt  3122  sbcrext  3123  sbcralg  3124  sbcrex  3125  sbcreug  3126  reu8nf  3127  cbvcsbv  3147  csbconstg  3155  nfcsb1v  3174  csbie  3187  csbnestg  3196  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  cbvralv2  3208  cbvrexv2  3209  dfss4st  3458  n0rf  3525  n0r  3526  eq0  3531  raaanlem  3618  nfpw  3690  cbviunv  4035  cbviinv  4036  ssiun2s  4040  iunab  4043  ssiinf  4046  ssiin  4047  iinab  4058  cbvdisjv  4101  nfdisjv  4102  disjnims  4105  disji2  4106  invdisjrab  4108  cbvmptv  4211  triun  4226  csbexga  4243  repizf2  4280  moop2  4373  euotd  4376  opelopabgf  4393  opelopabf  4398  nfpo  4427  nfso  4428  pofun  4438  nfse  4467  nffrfor  4474  nffr  4475  frind  4478  nfwe  4481  eusvnf  4579  rabxfrd  4595  tfis  4710  tfisi  4714  opeliunxp  4810  nfrel  4840  opeliunxp2  4900  ralxpf  4906  rexxpf  4907  nfco  4925  nfcnv  4939  dfdmf  4954  dfrnf  5003  nfdm  5006  nfres  5045  resmptf  5093  nfiotadw  5320  dffun6f  5370  dffun6  5371  dffun4f  5373  nffun  5380  funimaexglem  5444  nffv  5685  nffvmpt1  5686  dffn5imf  5737  funfvdm2f  5747  fvmptss2  5757  fvmpts  5760  fvmpt2  5766  fvmptssdm  5767  mptfvex  5768  fvmptdv  5771  fvmptd3  5776  elfvmptrab1  5777  eqfnfv2f  5784  ralrnmpt  5824  rexrnmpt  5825  f1ompt  5833  ffnfvf  5841  fmptco  5848  fmptcof  5849  fmptcos  5850  dfimafnf  5928  funiunfvdmf  5943  dff13f  5949  f1mpt  5950  fliftfuns  5977  nfiso  5985  nfriotadxy  6020  csbriotag  6025  riota2  6035  mpoeq123  6120  cbvmpox  6139  cbvmpo  6140  cbvmpov  6141  ovmpos  6185  ov2gf  6186  ovmpodxf  6187  ovmpodx  6188  ovmpodv  6194  ovmpodv2  6195  fvmpopr2d  6198  ovi3  6199  elovmporab  6262  elovmporab1w  6263  nfof  6281  nfofr  6282  offval2  6291  ofrfval2  6292  abrexex2g  6322  abrexex2  6326  uchoice  6344  dfopab2  6396  dfoprab3s  6397  mpomptsx  6406  dmmpossx  6408  fmpox  6409  mpofvex  6414  fnmpoovd  6424  fmpoco  6425  dfmpo  6432  f1od2  6444  disjxp1  6445  mpoxopoveq  6484  mpoxopovel  6485  nftpos  6523  tposoprab  6524  nfrecs  6551  nffrec  6640  eqerlem  6811  qliftfuns  6866  cbvixpv  6964  nfixpxy  6965  nfixp1  6966  ixpf  6968  mptelixpg  6982  dom2lem  7024  modom  7074  xpcomco  7090  xpf1o  7110  mapxpen  7114  ac6sfi  7168  opabfi  7213  nfsup  7296  nfdju  7346  exmidomni  7446  ismkvnex  7459  cc2  7597  cc4f  7599  cc4  7600  caucvgprprlemaddq  8039  caucvgsrlemgt1  8126  axpre-suploclemres  8232  lble  9238  supinfneg  9945  infsupneg  9946  fzrevral  10461  zsupcllemstep  10611  infssuzex  10615  infssuzcldc  10617  infssfzcldc  10618  infssfzledc  10619  nfseq  10843  seq3f1olemstep  10900  seq3f1olemp  10901  nfwrd  11278  reuccatpfxs1v  11465  fimaxre2  11937  nfsum1  12066  nfsum  12067  cbvsumv  12071  cbvsumi  12072  sumfct  12084  sumrbdclem  12088  summodclem2a  12092  zsumdc  12095  fsum3  12098  isumss  12102  isumss2  12104  fsum3cvg2  12105  fsumzcl2  12116  fsumadd  12117  fsumsplitf  12119  sumsnf  12120  sumsn  12122  sumsns  12126  fsumsplitsnun  12130  fsum2dlemstep  12145  fisumcom2  12149  fsumshftm  12156  fsum00  12173  fsumrelem  12182  fsumiun  12188  mertenslem2  12247  prodeq1  12264  nfcprod1  12265  nfcprod  12266  cbvprod  12269  cbvprodv  12270  cbvprodi  12271  prodrbdclem  12282  prodmodclem2a  12287  zproddc  12290  fprodseq  12294  fprodntrivap  12295  prodfct  12298  prodssdc  12300  prodsnf  12303  prodsn  12304  fprodm1s  12312  fprodp1s  12313  prodsns  12314  fprodcllemf  12324  fprodconst  12331  fprodap0  12332  fprod2dlemstep  12333  fprodcom2fi  12337  fprodrec  12340  fproddivapf  12342  fprodsplitf  12343  fprodap0f  12347  fprodle  12351  bezoutlemmain  12719  bezout  12732  nnwofdc  12759  nnwosdc  12760  prmind2  12842  oddpwdclemdvds  12892  oddpwdclemndvds  12893  pcmpt  13066  pcmptdvds  13068  ctiunctlemudc  13272  ctiunctlemf  13273  ctiunctlemfo  13274  ctiunct  13275  ctiunctal  13276  gsumfzconstf  14095  gsumsplit0  14099  gfsumsn  14107  prdsbas3  14129  cnmpt11  15274  cnmpt1t  15276  cnmpt21  15282  cnmpt2t  15284  cnmptcom  15289  imasnopn  15290  fsumcncntop  15558  ellimc3apf  15651  ellimc3ap  15652  limcmpted  15654  dvmptfsum  15716  elplyd  15732  fsumdvdsmul  15985  lgseisenlem2  16070  gropd  16168  grstructd2dom  16169  lfgrnloopen  16254  elabf1  16679  elabf2  16680  elabg2  16683  bj-omssind  16831  bj-bdfindisg  16844  bj-nntrans  16847  bj-nnelirr  16849  bj-omtrans  16852  setindis  16863  bdsetindis  16865  bj-nn0sucALT  16874  bj-findis  16875  bj-findisg  16876  strcollnfALT  16882  isomninnlem  16940  trilpolemeq1  16950  trirec0  16954  iswomninnlem  16960  ismkvnnlem  16963  nconstwlpolemgt0  16976