Theorem nfcv 2151

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 1394	. 2 ⊢ Ⅎx y ∈ A
2	1	nfci 2141	1 ⊢ ℲxA

Syntax hints:   ∈ wcel 1366  Ⅎwnfc 2138

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 1311  ax-17 1392

This theorem depends on definitions:  df-bi 110  df-nf 1323  df-nfc 2140

This theorem is referenced by:  nfcvd  2152  nfel  2159  nfeq1  2160  nfel1  2161  nfeq2  2162  nfel2  2163  nfcvf  2172  r2al  2312  r2ex  2313  nfraldxy  2325  nfrexdxy  2326  nfra2xy  2333  r19.12  2391  ralcom  2442  rexcom  2443  nfreudxy  2452  raleq  2474  rexeq  2475  reueq1  2476  rmoeq1  2477  cbvral  2498  cbvrex  2499  rabeq  2520  cbvrabv  2525  vtoclg  2581  vtocl2g  2585  vtoclga  2587  vtocl2ga  2589  vtocl3ga  2591  spcimdv  2605  spcimedv  2607  spcgv  2608  spcegv  2609  rspct  2617  rspc  2618  rspce  2619  rspc2  2629  ceqsexg  2640  elabgt  2652  elabf  2654  elabg  2656  elab3g  2661  elrab  2666  mob  2691  nfsbc1v  2750  elrabsf  2769  sbcralt  2802  sbcrext  2803  sbcralg  2804  sbcrexg  2805  sbcreug  2806  cbvcsbv  2825  csbconstg  2832  nfcsb1v  2850  csbnestg  2868  cbvralcsf  2876  cbvrexcsf  2877  cbvreucsf  2878  cbvrabcsf  2879  cbvralv2  2880  cbvrexv2  2881  n0rf  3201  n0r  3202  eq0  3207  raaanlem  3294  nfpw  3335  cbviunv  3659  cbviinv  3660  ssiun2s  3664  iunab  3666  ssiinf  3669  ssiin  3670  iinab  3681  cbvdisjv  3719  nfdisjv  3720  cbvmptv  3815  triun  3830  csbexga  3848  repizf2  3878  moop2  3951  euotd  3954  opelopabf  3974  nfpo  4001  nfso  4002  pofun  4012  nfse  4035  eusvnf  4123  rabxfrd  4139  tfis  4221  tfisi  4225  opeliunxp  4310  nfrel  4340  opeliunxp2  4391  ralxpf  4397  rexxpf  4398  nfco  4416  nfcnv  4429  dfdmf  4443  dfrnf  4490  nfdm  4493  nfres  4529  nfiotadxy  4785  dffun6f  4829  dffun6  4830  dffun4f  4832  nffun  4838  funimaexglem  4896  nffv  5098  nffvmpt1  5099  dffn5imf  5141  funfvdm2f  5151  fvmptss2  5160  fvmpts  5163  fvmpt2  5167  fvmptssdm  5168  mptfvex  5169  fvmptdv  5172  eqfnfv2f  5182  ralrnmpt  5222  rexrnmpt  5223  f1ompt  5233  ffnfvf  5237  fmptco  5243  fmptcof  5244  fmptcos  5245  funiunfvdmf  5316  dff13f  5322  f1mpt  5323  fliftfuns  5351  nfiso  5359  nfriotadxy  5388  csbriotag  5392  riota2  5402  mpt2eq123  5475  cbvmpt2x  5493  cbvmpt2  5494  cbvmpt2v  5495  ovmpt2s  5535  ov2gf  5536  ovmpt2dxf  5537  ovmpt2dx  5538  ovmpt2dv  5544  ovmpt2dv2  5545  ovi3  5548  nfof  5628  nfofr  5629  offval2  5637  ofrfval2  5638  abrexex2g  5658  abrexex2  5662  dfopab2  5726  dfoprab3s  5727  mpt2mptsx  5734  dmmpt2ssx  5736  fmpt2x  5737  mpt2fvex  5740  fmpt2co  5748  dfmpt2  5755  mpt2xopoveq  5765  mpt2xopovel  5766  nftpos  5804  tposoprab  5805  nfrecs  5832  eqerlem  6036  qliftfuns  6089  elabf1  8185  elabf2  8186  elabg2  8189  bj-omssind  8319  bj-bdfindisg  8332  bj-nntrans  8335  bj-nnelirr  8337  bj-omtrans  8340  setindis  8347  bdsetindis  8349  bj-nn0sucALT  8358  bj-findis  8359  bj-findisg  8360  strcollnfALT  8366