Theorem nfcv 2178

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

Syntax hints:   ∈ wcel 1393  Ⅎwnfc 2165

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338  ax-17 1419

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-nfc 2167

This theorem is referenced by:  nfcvd  2179  nfel  2186  nfeq1  2187  nfel1  2188  nfeq2  2189  nfel2  2190  nfcvf  2199  r2al  2343  r2ex  2344  nfraldxy  2356  nfrexdxy  2357  nfra2xy  2364  r19.12  2422  ralcom  2473  rexcom  2474  nfreudxy  2483  raleq  2505  rexeq  2506  reueq1  2507  rmoeq1  2508  cbvral  2529  cbvrex  2530  rabeq  2551  cbvrabv  2556  vtoclg  2613  vtocl2g  2617  vtoclga  2619  vtocl2ga  2621  vtocl3ga  2623  spcimdv  2637  spcimedv  2639  spcgv  2640  spcegv  2641  rspct  2649  rspc  2650  rspce  2651  rspc2  2661  ceqsexg  2672  elabgt  2684  elabf  2686  elabg  2688  elab3g  2693  elrab  2698  mob  2723  nfsbc1v  2782  elrabsf  2801  sbcralt  2834  sbcrext  2835  sbcralg  2836  sbcrex  2837  sbcreug  2838  cbvcsbv  2857  csbconstg  2864  nfcsb1v  2882  csbnestg  2900  cbvralcsf  2908  cbvrexcsf  2909  cbvreucsf  2910  cbvrabcsf  2911  cbvralv2  2912  cbvrexv2  2913  n0rf  3233  n0r  3234  eq0  3239  raaanlem  3326  nfpw  3371  cbviunv  3696  cbviinv  3697  ssiun2s  3701  iunab  3703  ssiinf  3706  ssiin  3707  iinab  3718  cbvdisjv  3756  nfdisjv  3757  cbvmptv  3852  triun  3867  csbexga  3885  repizf2  3915  moop2  3988  euotd  3991  opelopabf  4011  nfpo  4038  nfso  4039  pofun  4049  nfse  4078  nffrfor  4085  nffr  4086  frind  4089  nfwe  4092  eusvnf  4185  rabxfrd  4201  tfis  4306  tfisi  4310  opeliunxp  4395  nfrel  4425  opeliunxp2  4476  ralxpf  4482  rexxpf  4483  nfco  4501  nfcnv  4514  dfdmf  4528  dfrnf  4575  nfdm  4578  nfres  4614  nfiotadxy  4870  dffun6f  4915  dffun6  4916  dffun4f  4918  nffun  4924  funimaexglem  4982  nffv  5185  nffvmpt1  5186  dffn5imf  5228  funfvdm2f  5238  fvmptss2  5247  fvmpts  5250  fvmpt2  5254  fvmptssdm  5255  mptfvex  5256  fvmptdv  5259  eqfnfv2f  5269  ralrnmpt  5309  rexrnmpt  5310  f1ompt  5320  ffnfvf  5324  fmptco  5330  fmptcof  5331  fmptcos  5332  funiunfvdmf  5403  dff13f  5409  f1mpt  5410  fliftfuns  5438  nfiso  5446  nfriotadxy  5476  csbriotag  5480  riota2  5490  mpt2eq123  5564  cbvmpt2x  5582  cbvmpt2  5583  cbvmpt2v  5584  ovmpt2s  5624  ov2gf  5625  ovmpt2dxf  5626  ovmpt2dx  5627  ovmpt2dv  5633  ovmpt2dv2  5634  ovi3  5637  nfof  5717  nfofr  5718  offval2  5726  ofrfval2  5727  abrexex2g  5747  abrexex2  5751  dfopab2  5815  dfoprab3s  5816  mpt2mptsx  5823  dmmpt2ssx  5825  fmpt2x  5826  mpt2fvex  5829  fmpt2co  5837  dfmpt2  5844  mpt2xopoveq  5855  mpt2xopovel  5856  nftpos  5894  tposoprab  5895  nfrecs  5922  nffrec  5982  eqerlem  6137  qliftfuns  6190  dom2lem  6252  xpcomco  6300  ac6sfi  6352  caucvgprprlemaddq  6806  caucvgsrlemgt1  6879  fzrevral  8967  nfiseq  9218  nfsum1  9875  nfsum  9876  elabf1  9920  elabf2  9921  elabg2  9924  bj-omssind  10059  bj-bdfindisg  10073  bj-nntrans  10076  bj-nnelirr  10078  bj-omtrans  10081  setindis  10092  bdsetindis  10094  bj-nn0sucALT  10103  bj-findis  10104  bj-findisg  10105  strcollnfALT  10111