Theorem nfcv 2375

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 2365	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:   ∈ wcel 2202  Ⅎwnfc 2362

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 2364

This theorem is referenced by:  nfcvd  2376  nfel  2384  nfeq1  2385  nfel1  2386  nfeq2  2387  nfel2  2388  nfcvf  2398  r2al  2552  r2ex  2553  nfraldxy  2566  nfrexdxy  2567  nfra2xy  2575  r19.12  2640  ralcom  2697  rexcom  2698  nfreudxy  2708  raleq  2731  rexeq  2732  reueq1  2733  rmoeq1  2734  cbvralw  2761  cbvrexw  2762  cbvral  2764  cbvrex  2765  rabeq  2795  rabeqi  2796  cbvrabv  2802  vtoclg  2865  vtocl2g  2869  vtoclga  2871  vtocl2ga  2873  vtocl3ga  2875  spcimdv  2891  spcimedv  2893  spcgv  2894  spcegv  2895  rspct  2904  rspc  2905  rspce  2906  rspc2  2922  ceqsexg  2935  elabgt  2948  elabf  2950  elabg  2953  elab3g  2958  elrab  2963  mob  2989  nfsbc1v  3051  elrabsf  3071  sbcralt  3109  sbcrext  3110  sbcralg  3111  sbcrex  3112  sbcreug  3113  reu8nf  3114  cbvcsbv  3134  csbconstg  3142  nfcsb1v  3161  csbie  3174  csbnestg  3183  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  cbvralv2  3195  cbvrexv2  3196  dfss4st  3442  n0rf  3509  n0r  3510  eq0  3515  raaanlem  3601  nfpw  3669  cbviunv  4014  cbviinv  4015  ssiun2s  4019  iunab  4022  ssiinf  4025  ssiin  4026  iinab  4037  cbvdisjv  4080  nfdisjv  4081  disjnims  4084  disji2  4085  invdisjrab  4087  cbvmptv  4190  triun  4205  csbexga  4222  repizf2  4258  moop2  4350  euotd  4353  opelopabgf  4370  opelopabf  4375  nfpo  4404  nfso  4405  pofun  4415  nfse  4444  nffrfor  4451  nffr  4452  frind  4455  nfwe  4458  eusvnf  4556  rabxfrd  4572  tfis  4687  tfisi  4691  opeliunxp  4787  nfrel  4817  opeliunxp2  4876  ralxpf  4882  rexxpf  4883  nfco  4901  nfcnv  4915  dfdmf  4930  dfrnf  4979  nfdm  4982  nfres  5021  resmptf  5069  nfiotadw  5296  dffun6f  5346  dffun6  5347  dffun4f  5349  nffun  5356  funimaexglem  5420  nffv  5658  nffvmpt1  5659  dffn5imf  5710  funfvdm2f  5720  fvmptss2  5730  fvmpts  5733  fvmpt2  5739  fvmptssdm  5740  mptfvex  5741  fvmptdv  5744  fvmptd3  5749  elfvmptrab1  5750  eqfnfv2f  5757  ralrnmpt  5797  rexrnmpt  5798  f1ompt  5806  ffnfvf  5814  fmptco  5821  fmptcof  5822  fmptcos  5823  funiunfvdmf  5915  dff13f  5921  f1mpt  5922  fliftfuns  5949  nfiso  5957  nfriotadxy  5990  csbriotag  5995  riota2  6005  mpoeq123  6090  cbvmpox  6109  cbvmpo  6110  cbvmpov  6111  ovmpos  6155  ov2gf  6156  ovmpodxf  6157  ovmpodx  6158  ovmpodv  6164  ovmpodv2  6165  fvmpopr2d  6168  ovi3  6169  elovmporab  6232  elovmporab1w  6233  nfof  6250  nfofr  6251  offval2  6260  ofrfval2  6261  abrexex2g  6291  abrexex2  6295  uchoice  6309  dfopab2  6361  dfoprab3s  6362  mpomptsx  6371  dmmpossx  6373  fmpox  6374  mpofvex  6379  fnmpoovd  6389  fmpoco  6390  dfmpo  6397  f1od2  6409  disjxp1  6410  mpoxopoveq  6449  mpoxopovel  6450  nftpos  6488  tposoprab  6489  nfrecs  6516  nffrec  6605  eqerlem  6776  qliftfuns  6831  cbvixpv  6928  nfixpxy  6929  nfixp1  6930  ixpf  6932  mptelixpg  6946  dom2lem  6988  modom  7037  xpcomco  7053  xpf1o  7073  mapxpen  7077  ac6sfi  7130  opabfi  7175  nfsup  7234  nfdju  7284  exmidomni  7384  ismkvnex  7397  cc2  7529  cc4f  7531  cc4  7532  caucvgprprlemaddq  7971  caucvgsrlemgt1  8058  axpre-suploclemres  8164  lble  9169  supinfneg  9873  infsupneg  9874  fzrevral  10385  zsupcllemstep  10535  infssuzex  10539  infssuzcldc  10541  nfseq  10765  seq3f1olemstep  10822  seq3f1olemp  10823  nfwrd  11191  reuccatpfxs1v  11378  fimaxre2  11850  nfsum1  11979  nfsum  11980  cbvsumv  11984  cbvsumi  11985  sumfct  11997  sumrbdclem  12001  summodclem2a  12005  zsumdc  12008  fsum3  12011  isumss  12015  isumss2  12017  fsum3cvg2  12018  fsumzcl2  12029  fsumadd  12030  fsumsplitf  12032  sumsnf  12033  sumsn  12035  sumsns  12039  fsumsplitsnun  12043  fsum2dlemstep  12058  fisumcom2  12062  fsumshftm  12069  fsum00  12086  fsumrelem  12095  fsumiun  12101  mertenslem2  12160  prodeq1  12177  nfcprod1  12178  nfcprod  12179  cbvprod  12182  cbvprodv  12183  cbvprodi  12184  prodrbdclem  12195  prodmodclem2a  12200  zproddc  12203  fprodseq  12207  fprodntrivap  12208  prodfct  12211  prodssdc  12213  prodsnf  12216  prodsn  12217  fprodm1s  12225  fprodp1s  12226  prodsns  12227  fprodcllemf  12237  fprodconst  12244  fprodap0  12245  fprod2dlemstep  12246  fprodcom2fi  12250  fprodrec  12253  fproddivapf  12255  fprodsplitf  12256  fprodap0f  12260  fprodle  12264  bezoutlemmain  12632  bezout  12645  nnwofdc  12672  nnwosdc  12673  prmind2  12755  oddpwdclemdvds  12805  oddpwdclemndvds  12806  pcmpt  12979  pcmptdvds  12981  ctiunctlemudc  13121  ctiunctlemf  13122  ctiunctlemfo  13123  ctiunct  13124  ctiunctal  13125  prdsbas3  13433  gsumfzconstf  13992  gsumsplit0  13996  cnmpt11  15077  cnmpt1t  15079  cnmpt21  15085  cnmpt2t  15087  cnmptcom  15092  imasnopn  15093  fsumcncntop  15361  ellimc3apf  15454  ellimc3ap  15455  limcmpted  15457  dvmptfsum  15519  elplyd  15535  fsumdvdsmul  15788  lgseisenlem2  15873  gropd  15971  grstructd2dom  15972  lfgrnloopen  16057  elabf1  16482  elabf2  16483  elabg2  16486  bj-omssind  16634  bj-bdfindisg  16647  bj-nntrans  16650  bj-nnelirr  16652  bj-omtrans  16655  setindis  16666  bdsetindis  16668  bj-nn0sucALT  16677  bj-findis  16678  bj-findisg  16679  strcollnfALT  16685  isomninnlem  16745  trilpolemeq1  16755  trirec0  16759  iswomninnlem  16765  ismkvnnlem  16768  nconstwlpolemgt0  16780  gfsumsn  16797