Theorem nfcv 2336

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

Syntax hints:   ∈ wcel 2164  Ⅎwnfc 2323

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 1460  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-nfc 2325

This theorem is referenced by:  nfcvd  2337  nfel  2345  nfeq1  2346  nfel1  2347  nfeq2  2348  nfel2  2349  nfcvf  2359  r2al  2513  r2ex  2514  nfraldxy  2527  nfrexdxy  2528  nfra2xy  2536  r19.12  2600  ralcom  2657  rexcom  2658  nfreudxy  2668  raleq  2690  rexeq  2691  reueq1  2692  rmoeq1  2693  cbvralw  2720  cbvrexw  2721  cbvral  2722  cbvrex  2723  rabeq  2752  rabeqi  2753  cbvrabv  2759  vtoclg  2821  vtocl2g  2825  vtoclga  2827  vtocl2ga  2829  vtocl3ga  2831  spcimdv  2845  spcimedv  2847  spcgv  2848  spcegv  2849  rspct  2858  rspc  2859  rspce  2860  rspc2  2876  ceqsexg  2889  elabgt  2902  elabf  2904  elabg  2907  elab3g  2912  elrab  2917  mob  2943  nfsbc1v  3005  elrabsf  3025  sbcralt  3063  sbcrext  3064  sbcralg  3065  sbcrex  3066  sbcreug  3067  cbvcsbv  3087  csbconstg  3095  nfcsb1v  3114  csbie  3127  csbnestg  3136  cbvralcsf  3144  cbvrexcsf  3145  cbvreucsf  3146  cbvrabcsf  3147  cbvralv2  3148  cbvrexv2  3149  dfss4st  3393  n0rf  3460  n0r  3461  eq0  3466  raaanlem  3552  nfpw  3615  cbviunv  3952  cbviinv  3953  ssiun2s  3957  iunab  3960  ssiinf  3963  ssiin  3964  iinab  3975  cbvdisjv  4018  nfdisjv  4019  disjnims  4022  disji2  4023  cbvmptv  4126  triun  4141  csbexga  4158  repizf2  4192  moop2  4281  euotd  4284  opelopabgf  4301  opelopabf  4306  nfpo  4333  nfso  4334  pofun  4344  nfse  4373  nffrfor  4380  nffr  4381  frind  4384  nfwe  4387  eusvnf  4485  rabxfrd  4501  tfis  4616  tfisi  4620  opeliunxp  4715  nfrel  4745  opeliunxp2  4803  ralxpf  4809  rexxpf  4810  nfco  4828  nfcnv  4842  dfdmf  4856  dfrnf  4904  nfdm  4907  nfres  4945  resmptf  4993  nfiotadw  5219  dffun6f  5268  dffun6  5269  dffun4f  5271  nffun  5278  funimaexglem  5338  nffv  5565  nffvmpt1  5566  dffn5imf  5613  funfvdm2f  5623  fvmptss2  5633  fvmpts  5636  fvmpt2  5642  fvmptssdm  5643  mptfvex  5644  fvmptdv  5647  fvmptd3  5652  elfvmptrab1  5653  eqfnfv2f  5660  ralrnmpt  5701  rexrnmpt  5702  f1ompt  5710  ffnfvf  5718  fmptco  5725  fmptcof  5726  fmptcos  5727  funiunfvdmf  5808  dff13f  5814  f1mpt  5815  fliftfuns  5842  nfiso  5850  nfriotadxy  5883  csbriotag  5887  riota2  5897  mpoeq123  5978  cbvmpox  5997  cbvmpo  5998  cbvmpov  5999  ovmpos  6043  ov2gf  6044  ovmpodxf  6045  ovmpodx  6046  ovmpodv  6052  ovmpodv2  6053  fvmpopr2d  6056  ovi3  6057  elovmporab  6120  elovmporab1w  6121  nfof  6138  nfofr  6139  offval2  6148  ofrfval2  6149  abrexex2g  6174  abrexex2  6178  uchoice  6192  dfopab2  6244  dfoprab3s  6245  mpomptsx  6252  dmmpossx  6254  fmpox  6255  mpofvex  6260  fnmpoovd  6270  fmpoco  6271  dfmpo  6278  f1od2  6290  disjxp1  6291  mpoxopoveq  6295  mpoxopovel  6296  nftpos  6334  tposoprab  6335  nfrecs  6362  nffrec  6451  eqerlem  6620  qliftfuns  6675  cbvixpv  6772  nfixpxy  6773  nfixp1  6774  ixpf  6776  mptelixpg  6790  dom2lem  6828  xpcomco  6882  xpf1o  6902  mapxpen  6906  ac6sfi  6956  opabfi  6994  nfsup  7053  nfdju  7103  exmidomni  7203  ismkvnex  7216  cc2  7329  cc4f  7331  cc4  7332  caucvgprprlemaddq  7770  caucvgsrlemgt1  7857  axpre-suploclemres  7963  lble  8968  supinfneg  9663  infsupneg  9664  fzrevral  10174  nfseq  10531  seq3f1olemstep  10588  seq3f1olemp  10589  nfwrd  10945  fimaxre2  11373  nfsum1  11502  nfsum  11503  cbvsumv  11507  cbvsumi  11508  sumfct  11520  sumrbdclem  11523  summodclem2a  11527  zsumdc  11530  fsum3  11533  isumss  11537  isumss2  11539  fsum3cvg2  11540  fsumzcl2  11551  fsumadd  11552  fsumsplitf  11554  sumsnf  11555  sumsn  11557  sumsns  11561  fsumsplitsnun  11565  fsum2dlemstep  11580  fisumcom2  11584  fsumshftm  11591  fsum00  11608  fsumrelem  11617  fsumiun  11623  mertenslem2  11682  prodeq1  11699  nfcprod1  11700  nfcprod  11701  cbvprod  11704  cbvprodv  11705  cbvprodi  11706  prodrbdclem  11717  prodmodclem2a  11722  zproddc  11725  fprodseq  11729  fprodntrivap  11730  prodfct  11733  prodssdc  11735  prodsnf  11738  prodsn  11739  fprodm1s  11747  fprodp1s  11748  prodsns  11749  fprodcllemf  11759  fprodconst  11766  fprodap0  11767  fprod2dlemstep  11768  fprodcom2fi  11772  fprodrec  11775  fproddivapf  11777  fprodsplitf  11778  fprodap0f  11782  fprodle  11786  zsupcllemstep  12085  infssuzex  12089  infssuzcldc  12091  bezoutlemmain  12138  bezout  12151  nnwofdc  12178  nnwosdc  12179  prmind2  12261  oddpwdclemdvds  12311  oddpwdclemndvds  12312  pcmpt  12484  pcmptdvds  12486  ctiunctlemudc  12597  ctiunctlemf  12598  ctiunctlemfo  12599  ctiunct  12600  ctiunctal  12601  gsumfzconstf  13415  cnmpt11  14462  cnmpt1t  14464  cnmpt21  14470  cnmpt2t  14472  cnmptcom  14477  imasnopn  14478  fsumcncntop  14746  ellimc3apf  14839  ellimc3ap  14840  limcmpted  14842  dvmptfsum  14904  elplyd  14920  lgseisenlem2  15228  elabf1  15343  elabf2  15344  elabg2  15347  bj-omssind  15497  bj-bdfindisg  15510  bj-nntrans  15513  bj-nnelirr  15515  bj-omtrans  15518  setindis  15529  bdsetindis  15531  bj-nn0sucALT  15540  bj-findis  15541  bj-findisg  15542  strcollnfALT  15548  isomninnlem  15590  trilpolemeq1  15600  trirec0  15604  iswomninnlem  15609  ismkvnnlem  15612  nconstwlpolemgt0  15624