Theorem nfcv 2156

Description: If x is disjoint from A, then x is not free in A. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfcv	⊢ ℲxA

Distinct variable group:   x,A

Proof of Theorem nfcv

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1398	. 2 ⊢ Ⅎx y ∈ A
2	1	nfci 2146	1 ⊢ ℲxA

Syntax hints:   ∈ wcel 1370  Ⅎwnfc 2143

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 1314  ax-17 1396

This theorem depends on definitions:  df-bi 110  df-nf 1326  df-nfc 2145

This theorem is referenced by:  nfcvd  2157  nfel  2164  nfeq1  2165  nfel1  2166  nfeq2  2167  nfel2  2168  nfcvf  2177  r2al  2317  r2ex  2318  nfraldxy  2330  nfrexdxy  2331  nfra2xy  2338  r19.12  2396  ralcom  2447  rexcom  2448  nfreudxy  2457  raleq  2479  rexeq  2480  reueq1  2481  rmoeq1  2482  cbvral  2503  cbvrex  2504  rabeq  2525  cbvrabv  2530  vtoclg  2586  vtocl2g  2590  vtoclga  2592  vtocl2ga  2594  vtocl3ga  2596  spcimdv  2610  spcimedv  2612  spcgv  2613  spcegv  2614  rspct  2622  rspc  2623  rspce  2624  rspc2  2634  ceqsexg  2645  elabgt  2657  elabf  2659  elabg  2661  elab3g  2666  elrab  2671  mob  2696  nfsbc1v  2755  elrabsf  2774  sbcralt  2807  sbcrext  2808  sbcralg  2809  sbcrexg  2810  sbcreug  2811  cbvcsbv  2830  csbconstg  2837  nfcsb1v  2855  csbnestg  2873  cbvralcsf  2881  cbvrexcsf  2882  cbvreucsf  2883  cbvrabcsf  2884  cbvralv2  2885  cbvrexv2  2886  n0rf  3206  n0r  3207  eq0  3212  raaanlem  3301  nfpw  3342  cbviunv  3666  cbviinv  3667  ssiun2s  3671  iunab  3673  ssiinf  3676  ssiin  3677  iinab  3688  cbvdisjv  3726  nfdisjv  3727  cbvmptv  3822  triun  3837  csbexgOLD  3855  repizf2  3885  moop2  3958  euotd  3961  opelopabf  3981  nfpo  4008  nfso  4009  pofun  4019  nfse  4042  eusvnf  4131  rabxfrd  4147  tfis  4229  tfisi  4233  opeliunxp  4318  nfrel  4348  opeliunxp2  4399  ralxpf  4405  rexxpf  4406  nfco  4424  nfcnv  4437  dfdmf  4451  dfrnf  4498  nfdm  4501  nfres  4537  nfiotadxy  4793  dffun6f  4837  dffun6  4838  dffun4f  4840  nffun  4846  funimaexglem  4904  nffv  5106  nffvmpt1  5107  dffn5imf  5149  funfvdm2f  5159  fvmptss2  5168  fvmpts  5171  fvmpt2  5175  fvmptssdm  5176  mptfvex  5177  fvmptdv  5180  eqfnfv2f  5190  ralrnmpt  5230  rexrnmpt  5231  f1ompt  5241  ffnfvf  5245  fmptco  5251  fmptcof  5252  fmptcos  5253  funiunfvdmf  5324  dff13f  5330  f1mpt  5331  fliftfuns  5359  nfiso  5367  nfriotadxy  5396  csbriotag  5400  riota2  5410  mpt2eq123  5483  cbvmpt2x  5501  cbvmpt2  5502  cbvmpt2v  5503  ovmpt2s  5543  ov2gf  5544  ovmpt2dxf  5545  ovmpt2dx  5546  ovmpt2dv  5552  ovmpt2dv2  5553  ovi3  5556  nfof  5636  nfofr  5637  offval2  5645  ofrfval2  5646  abrexex2g  5666  abrexex2  5670  dfopab2  5734  dfoprab3s  5735  mpt2mptsx  5742  dmmpt2ssx  5744  fmpt2x  5745  mpt2fvex  5748  fmpt2co  5756  dfmpt2  5763  mpt2xopoveq  5773  mpt2xopovel  5774  nftpos  5812  tposoprab  5813  nfrecs  5840  eqerlem  6044  qliftfuns  6097  elabf1  7166  elabf2  7167  elabg2  7170  bj-omssind  7296  bj-bdfindisg  7309  bj-nntrans  7312  bj-nnelirr  7314  bj-omtrans  7317  setindis  7324  bdsetindis  7326  bj-nn0sucALT  7335  bj-findis  7336  bj-findisg  7337  strcollnfALT  7343