Theorem nfcv 2392

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

This proof depends on syntax axioms:   ∈ wcel 2209  Ⅎwnfc 2379

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-nfc 2381

This theorem is used by:  nfcvd  2393  nfel  2401  nfeq1  2402  nfel1  2403  nfeq2  2404  nfel2  2405  nfcvf  2415  r2al  2569  r2ex  2570  nfraldxy  2583  nfrexdxy  2584  nfra2xy  2592  r19.12  2657  ralcom  2714  rexcom  2715  nfreudxy  2725  raleq  2749  rexeq  2750  reueq1  2751  rmoeq1  2752  cbvralw  2779  cbvrexw  2780  cbvral  2782  cbvrex  2783  rabeq  2813  rabeqi  2814  cbvrabv  2820  vtoclg  2883  vtocl2g  2887  vtoclga  2889  vtocl2ga  2891  vtocl3ga  2893  spcimdv  2909  spcimedv  2911  spcgv  2912  spcegv  2913  rspct  2922  rspc  2923  rspce  2924  rspc2  2941  ceqsexg  2954  elabgt  2967  elabf  2969  elabg  2972  elab3g  2977  elrab  2982  mob  3008  nfsbc1v  3070  elrabsf  3090  sbcralt  3128  sbcrext  3129  sbcralg  3130  sbcrex  3131  sbcreug  3132  reu8nf  3133  cbvcsbv  3153  csbconstg  3161  nfcsb1v  3180  csbie  3193  csbnestg  3202  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  cbvralv2  3214  cbvrexv2  3215  dfss4st  3464  n0rf  3534  n0r  3535  eq0  3540  raaanlem  3632  nfpw  3705  cbviunv  4051  cbviinv  4052  ssiun2s  4056  iunab  4059  ssiinf  4062  ssiin  4063  iinab  4074  cbvdisjv  4117  nfdisjv  4118  disjnims  4121  disji2  4122  invdisjrab  4124  cbvmptv  4227  triun  4242  csbexga  4261  repizf2  4299  moop2  4392  euotd  4395  opelopabgf  4412  opelopabf  4417  nfpo  4446  nfso  4447  pofun  4457  nfse  4486  nffrfor  4493  nffr  4494  frind  4497  nfwe  4500  eusvnf  4599  rabxfrd  4615  tfis  4730  tfisi  4734  opeliunxp  4830  nfrel  4860  opeliunxp2  4920  ralxpf  4926  rexxpf  4927  nfco  4945  nfcnv  4959  dfdmf  4974  dfrnf  5023  nfdm  5026  nfres  5065  resmptf  5113  nfiotadw  5340  dffun6f  5390  dffun6  5391  dffun4f  5393  nffun  5400  funimaexglem  5464  nffv  5705  nffvmpt1  5706  dffn5imf  5758  funfvdm2f  5768  fvmptss2  5780  fvmpts  5783  fvmpt2  5789  fvmptssdm  5790  mptfvex  5791  fvmptdv  5794  fvmptd3  5799  elfvmptrab1  5801  eqfnfv2f  5810  ralrnmpt  5850  rexrnmpt  5851  f1ompt  5859  ffnfvf  5867  fmptco  5874  fmptcof  5875  fmptcos  5876  dfimafnf  5955  funiunfvdmf  5970  dff13f  5976  f1mpt  5977  fliftfuns  6004  nfiso  6012  nfriotadxy  6047  csbriotag  6052  riota2  6062  mpoeq123  6147  cbvmpox  6166  cbvmpo  6167  cbvmpov  6168  ovmpos  6212  ov2gf  6213  ovmpodxf  6214  ovmpodx  6215  ovmpodv  6221  ovmpodv2  6222  fvmpopr2d  6225  ovi3  6226  elovmporab  6289  elovmporab1w  6290  nfof  6308  nfofr  6309  offval2  6318  ofrfval2  6319  abrexex2g  6349  abrexex2  6353  uchoice  6371  dfopab2  6423  dfoprab3s  6424  mpomptsx  6433  dmmpossx  6435  fmpox  6436  mpofvex  6441  fnmpoovd  6451  fmpoco  6452  dfmpo  6459  f1od2  6471  disjxp1  6472  mpoxopoveq  6511  mpoxopovel  6512  nftpos  6550  tposoprab  6551  nfrecs  6578  nffrec  6667  eqerlem  6838  qliftfuns  6893  cbvixpv  6998  nfixpxy  6999  nfixp1  7000  ixpf  7002  mptelixpg  7016  dom2lem  7058  modom  7108  xpcomco  7124  xpf1o  7144  mapxpen  7148  ac6sfi  7202  opabfi  7247  nfsup  7332  nfdju  7382  exmidomni  7482  ismkvnex  7495  cc2  7633  cc4f  7635  cc4  7636  caucvgprprlemaddq  8075  caucvgsrlemgt1  8162  axpre-suploclemres  8268  lble  9277  supinfneg  9995  infsupneg  9996  fzrevral  10512  zsupcllemstep  10662  infssuzex  10666  infssuzcldc  10668  infssfzcldc  10669  infssfzledc  10670  nfseq  10894  seq3f1olemstep  10951  seq3f1olemp  10952  nfwrd  11333  reuccatpfxs1v  11520  fimaxre2  11993  nfsum1  12122  nfsum  12123  cbvsumv  12127  cbvsumi  12128  sumfct  12140  sumrbdclem  12144  summodclem2a  12148  zsumdc  12151  fsum3  12154  isumss  12158  isumss2  12160  fsum3cvg2  12161  fsumzcl2  12172  fsumadd  12173  fsumsplitf  12175  sumsnf  12176  sumsn  12178  sumsns  12182  fsumsplitsnun  12186  fsum2dlemstep  12201  fisumcom2  12205  fsumshftm  12212  fsum00  12229  fsumrelem  12238  fsumiun  12244  mertenslem2  12303  prodeq1  12320  nfcprod1  12321  nfcprod  12322  cbvprod  12325  cbvprodv  12326  cbvprodi  12327  prodrbdclem  12338  prodmodclem2a  12343  zproddc  12346  fprodseq  12350  fprodntrivap  12351  prodfct  12354  prodssdc  12356  prodsnf  12359  prodsn  12360  fprodm1s  12368  fprodp1s  12369  prodsns  12370  fprodcllemf  12380  fprodconst  12387  fprodap0  12388  fprod2dlemstep  12389  fprodcom2fi  12393  fprodrec  12396  fproddivapf  12398  fprodsplitf  12399  fprodap0f  12403  fprodle  12407  bezoutlemmain  12775  bezout  12788  nnwofdc  12815  nnwosdc  12816  prmind2  12898  oddpwdclemdvds  12948  oddpwdclemndvds  12949  pcmpt  13122  pcmptdvds  13124  ctiunctlemudc  13328  ctiunctlemf  13329  ctiunctlemfo  13330  ctiunct  13331  ctiunctal  13332  gzsumconstf  14144  gzsumsplit0  14148  gsumsncmn  14156  gsummptfidmadd  14161  prdsbas3  14187  cnmpt11  15384  cnmpt1t  15386  cnmpt21  15392  cnmpt2t  15394  cnmptcom  15399  imasnopn  15400  fsumcncntop  15668  ellimc3apf  15761  ellimc3ap  15762  limcmpted  15764  dvmptfsum  15826  elplyd  15842  fsumdvdsmul  16105  lgseisenlem2  16190  gropd  16288  grstructd2dom  16289  lfgrnloopen  16374  elabf1  16809  elabf2  16810  elabg2  16813  bj-omssind  16961  bj-bdfindisg  16974  bj-nntrans  16977  bj-nnelirr  16979  bj-omtrans  16982  setindis  16993  bdsetindis  16995  bj-nn0sucALT  17004  bj-findis  17005  bj-findisg  17006  strcollnfALT  17012  isomninnlem  17079  trilpolemeq1  17089  trirec0  17093  iswomninnlem  17099  ismkvnnlem  17102  nconstwlpolemgt0  17114