Theorem nfcv 2225

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

Syntax hints:   ∈ wcel 1436  Ⅎwnfc 2212

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1381  ax-17 1462

This theorem depends on definitions:  df-bi 115  df-nf 1393  df-nfc 2214

This theorem is referenced by:  nfcvd  2226  nfel  2233  nfeq1  2234  nfel1  2235  nfeq2  2236  nfel2  2237  nfcvf  2246  r2al  2393  r2ex  2394  nfraldxy  2406  nfrexdxy  2407  nfra2xy  2414  r19.12  2474  ralcom  2526  rexcom  2527  nfreudxy  2536  raleq  2558  rexeq  2559  reueq1  2560  rmoeq1  2561  cbvral  2582  cbvrex  2583  rabeq  2607  rabeqi  2608  cbvrabv  2614  vtoclg  2672  vtocl2g  2676  vtoclga  2678  vtocl2ga  2680  vtocl3ga  2682  spcimdv  2696  spcimedv  2698  spcgv  2699  spcegv  2700  rspct  2708  rspc  2709  rspce  2710  rspc2  2724  ceqsexg  2736  elabgt  2748  elabf  2750  elabg  2752  elab3g  2757  elrab  2762  mob  2788  nfsbc1v  2847  elrabsf  2866  sbcralt  2904  sbcrext  2905  sbcralg  2906  sbcrex  2907  sbcreug  2908  cbvcsbv  2927  csbconstg  2934  nfcsb1v  2952  csbie  2962  csbnestg  2971  cbvralcsf  2979  cbvrexcsf  2980  cbvreucsf  2981  cbvrabcsf  2982  cbvralv2  2983  cbvrexv2  2984  dfss4st  3221  n0rf  3284  n0r  3285  eq0  3290  raaanlem  3374  nfpw  3427  cbviunv  3752  cbviinv  3753  ssiun2s  3757  iunab  3759  ssiinf  3762  ssiin  3763  iinab  3774  cbvdisjv  3812  nfdisjv  3813  cbvmptv  3909  triun  3924  csbexga  3942  repizf2  3972  moop2  4052  euotd  4055  opelopabf  4075  nfpo  4102  nfso  4103  pofun  4113  nfse  4142  nffrfor  4149  nffr  4150  frind  4153  nfwe  4156  eusvnf  4249  rabxfrd  4265  tfis  4371  tfisi  4375  opeliunxp  4461  nfrel  4491  opeliunxp2  4544  ralxpf  4550  rexxpf  4551  nfco  4569  nfcnv  4583  dfdmf  4597  dfrnf  4644  nfdm  4647  nfres  4683  resmptf  4729  nfiotadxy  4949  dffun6f  4994  dffun6  4995  dffun4f  4997  nffun  5003  funimaexglem  5062  nffv  5278  nffvmpt1  5279  dffn5imf  5322  funfvdm2f  5332  fvmptss2  5342  fvmpts  5345  fvmpt2  5349  fvmptssdm  5350  mptfvex  5351  fvmptdv  5354  eqfnfv2f  5364  ralrnmpt  5404  rexrnmpt  5405  f1ompt  5413  ffnfvf  5420  fmptco  5427  fmptcof  5428  fmptcos  5429  funiunfvdmf  5504  dff13f  5510  f1mpt  5511  fliftfuns  5538  nfiso  5546  nfriotadxy  5577  csbriotag  5581  riota2  5591  mpt2eq123  5665  cbvmpt2x  5683  cbvmpt2  5684  cbvmpt2v  5685  ovmpt2s  5725  ov2gf  5726  ovmpt2dxf  5727  ovmpt2dx  5728  ovmpt2dv  5734  ovmpt2dv2  5735  ovi3  5738  nfof  5818  nfofr  5819  offval2  5827  ofrfval2  5828  abrexex2g  5848  abrexex2  5852  dfopab2  5916  dfoprab3s  5917  mpt2mptsx  5924  dmmpt2ssx  5926  fmpt2x  5927  mpt2fvex  5930  fmpt2co  5938  dfmpt2  5945  f1od2  5957  mpt2xopoveq  5959  mpt2xopovel  5960  nftpos  5998  tposoprab  5999  nfrecs  6026  nffrec  6115  eqerlem  6275  qliftfuns  6328  dom2lem  6441  xpcomco  6494  xpf1o  6512  mapxpen  6516  ac6sfi  6566  nfsup  6631  nfdju  6679  exmidomni  6742  caucvgprprlemaddq  7211  caucvgsrlemgt1  7284  lble  8343  supinfneg  9015  infsupneg  9016  fzrevral  9449  nfiseq  9786  iseqf1olemstep  9834  iseqf1olemp  9835  fimaxre2  10551  nfsum1  10635  nfsum  10636  cbvsumv  10640  cbvsumi  10641  sumfct  10653  isumrblem  10655  isummolem2a  10660  zisum  10663  fisum  10665  isumss  10669  zsupcllemstep  10816  infssuzex  10820  infssuzcldc  10822  bezoutlemmain  10862  bezout  10875  prmind2  10977  oddpwdclemdvds  11023  oddpwdclemndvds  11024  elabf1  11119  elabf2  11120  elabg2  11123  bj-omssind  11268  bj-bdfindisg  11281  bj-nntrans  11284  bj-nnelirr  11286  bj-omtrans  11289  setindis  11300  bdsetindis  11302  bj-nn0sucALT  11311  bj-findis  11312  bj-findisg  11313  strcollnfALT  11319