Theorem nfcv 2175

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

Syntax hints:   ∈ wcel 1390  Ⅎwnfc 2162

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 1335  ax-17 1416

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-nfc 2164

This theorem is referenced by:  nfcvd  2176  nfel  2183  nfeq1  2184  nfel1  2185  nfeq2  2186  nfel2  2187  nfcvf  2196  r2al  2337  r2ex  2338  nfraldxy  2350  nfrexdxy  2351  nfra2xy  2358  r19.12  2416  ralcom  2467  rexcom  2468  nfreudxy  2477  raleq  2499  rexeq  2500  reueq1  2501  rmoeq1  2502  cbvral  2523  cbvrex  2524  rabeq  2545  cbvrabv  2550  vtoclg  2607  vtocl2g  2611  vtoclga  2613  vtocl2ga  2615  vtocl3ga  2617  spcimdv  2631  spcimedv  2633  spcgv  2634  spcegv  2635  rspct  2643  rspc  2644  rspce  2645  rspc2  2655  ceqsexg  2666  elabgt  2678  elabf  2680  elabg  2682  elab3g  2687  elrab  2692  mob  2717  nfsbc1v  2776  elrabsf  2795  sbcralt  2828  sbcrext  2829  sbcralg  2830  sbcrexg  2831  sbcreug  2832  cbvcsbv  2851  csbconstg  2858  nfcsb1v  2876  csbnestg  2894  cbvralcsf  2902  cbvrexcsf  2903  cbvreucsf  2904  cbvrabcsf  2905  cbvralv2  2906  cbvrexv2  2907  n0rf  3227  n0r  3228  eq0  3233  raaanlem  3320  nfpw  3363  cbviunv  3687  cbviinv  3688  ssiun2s  3692  iunab  3694  ssiinf  3697  ssiin  3698  iinab  3709  cbvdisjv  3747  nfdisjv  3748  cbvmptv  3843  triun  3858  csbexga  3876  repizf2  3906  moop2  3979  euotd  3982  opelopabf  4002  nfpo  4029  nfso  4030  pofun  4040  nfse  4063  eusvnf  4151  rabxfrd  4167  tfis  4249  tfisi  4253  opeliunxp  4338  nfrel  4368  opeliunxp2  4419  ralxpf  4425  rexxpf  4426  nfco  4444  nfcnv  4457  dfdmf  4471  dfrnf  4518  nfdm  4521  nfres  4557  nfiotadxy  4813  dffun6f  4858  dffun6  4859  dffun4f  4861  nffun  4867  funimaexglem  4925  nffv  5128  nffvmpt1  5129  dffn5imf  5171  funfvdm2f  5181  fvmptss2  5190  fvmpts  5193  fvmpt2  5197  fvmptssdm  5198  mptfvex  5199  fvmptdv  5202  eqfnfv2f  5212  ralrnmpt  5252  rexrnmpt  5253  f1ompt  5263  ffnfvf  5267  fmptco  5273  fmptcof  5274  fmptcos  5275  funiunfvdmf  5346  dff13f  5352  f1mpt  5353  fliftfuns  5381  nfiso  5389  nfriotadxy  5419  csbriotag  5423  riota2  5433  mpt2eq123  5506  cbvmpt2x  5524  cbvmpt2  5525  cbvmpt2v  5526  ovmpt2s  5566  ov2gf  5567  ovmpt2dxf  5568  ovmpt2dx  5569  ovmpt2dv  5575  ovmpt2dv2  5576  ovi3  5579  nfof  5659  nfofr  5660  offval2  5668  ofrfval2  5669  abrexex2g  5689  abrexex2  5693  dfopab2  5757  dfoprab3s  5758  mpt2mptsx  5765  dmmpt2ssx  5767  fmpt2x  5768  mpt2fvex  5771  fmpt2co  5779  dfmpt2  5786  mpt2xopoveq  5796  mpt2xopovel  5797  nftpos  5835  tposoprab  5836  nfrecs  5863  nffrec  5921  eqerlem  6073  qliftfuns  6126  dom2lem  6188  xpcomco  6236  fzrevral  8737  nfiseq  8898  elabf1  9255  elabf2  9256  elabg2  9259  bj-omssind  9394  bj-bdfindisg  9408  bj-nntrans  9411  bj-nnelirr  9413  bj-omtrans  9416  setindis  9427  bdsetindis  9429  bj-nn0sucALT  9438  bj-findis  9439  bj-findisg  9440  strcollnfALT  9446