Theorem nfcv 2219

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

Syntax hints:   ∈ wcel 1433  Ⅎwnfc 2206

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 1378  ax-17 1459

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-nfc 2208

This theorem is referenced by:  nfcvd  2220  nfel  2227  nfeq1  2228  nfel1  2229  nfeq2  2230  nfel2  2231  nfcvf  2240  r2al  2385  r2ex  2386  nfraldxy  2398  nfrexdxy  2399  nfra2xy  2406  r19.12  2466  ralcom  2517  rexcom  2518  nfreudxy  2527  raleq  2549  rexeq  2550  reueq1  2551  rmoeq1  2552  cbvral  2573  cbvrex  2574  rabeq  2595  cbvrabv  2600  vtoclg  2658  vtocl2g  2662  vtoclga  2664  vtocl2ga  2666  vtocl3ga  2668  spcimdv  2682  spcimedv  2684  spcgv  2685  spcegv  2686  rspct  2694  rspc  2695  rspce  2696  rspc2  2711  ceqsexg  2723  elabgt  2735  elabf  2737  elabg  2739  elab3g  2744  elrab  2749  mob  2774  nfsbc1v  2833  elrabsf  2852  sbcralt  2890  sbcrext  2891  sbcralg  2892  sbcrex  2893  sbcreug  2894  cbvcsbv  2913  csbconstg  2920  nfcsb1v  2938  csbnestg  2956  cbvralcsf  2964  cbvrexcsf  2965  cbvreucsf  2966  cbvrabcsf  2967  cbvralv2  2968  cbvrexv2  2969  n0rf  3260  n0r  3261  eq0  3266  raaanlem  3346  nfpw  3394  cbviunv  3717  cbviinv  3718  ssiun2s  3722  iunab  3724  ssiinf  3727  ssiin  3728  iinab  3739  cbvdisjv  3777  nfdisjv  3778  cbvmptv  3873  triun  3888  csbexga  3906  repizf2  3936  moop2  4006  euotd  4009  opelopabf  4029  nfpo  4056  nfso  4057  pofun  4067  nfse  4096  nffrfor  4103  nffr  4104  frind  4107  nfwe  4110  eusvnf  4203  rabxfrd  4219  tfis  4324  tfisi  4328  opeliunxp  4413  nfrel  4443  opeliunxp2  4494  ralxpf  4500  rexxpf  4501  nfco  4519  nfcnv  4532  dfdmf  4546  dfrnf  4593  nfdm  4596  nfres  4632  nfiotadxy  4890  dffun6f  4935  dffun6  4936  dffun4f  4938  nffun  4944  funimaexglem  5002  nffv  5205  nffvmpt1  5206  dffn5imf  5249  funfvdm2f  5259  fvmptss2  5268  fvmpts  5271  fvmpt2  5275  fvmptssdm  5276  mptfvex  5277  fvmptdv  5280  eqfnfv2f  5290  ralrnmpt  5330  rexrnmpt  5331  f1ompt  5341  ffnfvf  5345  fmptco  5351  fmptcof  5352  fmptcos  5353  funiunfvdmf  5424  dff13f  5430  f1mpt  5431  fliftfuns  5458  nfiso  5466  nfriotadxy  5496  csbriotag  5500  riota2  5510  mpt2eq123  5584  cbvmpt2x  5602  cbvmpt2  5603  cbvmpt2v  5604  ovmpt2s  5644  ov2gf  5645  ovmpt2dxf  5646  ovmpt2dx  5647  ovmpt2dv  5653  ovmpt2dv2  5654  ovi3  5657  nfof  5737  nfofr  5738  offval2  5746  ofrfval2  5747  abrexex2g  5767  abrexex2  5771  dfopab2  5835  dfoprab3s  5836  mpt2mptsx  5843  dmmpt2ssx  5845  fmpt2x  5846  mpt2fvex  5849  fmpt2co  5857  dfmpt2  5864  f1od2  5876  mpt2xopoveq  5878  mpt2xopovel  5879  nftpos  5917  tposoprab  5918  nfrecs  5945  nffrec  6005  eqerlem  6160  qliftfuns  6213  dom2lem  6275  xpcomco  6323  ac6sfi  6379  nfsup  6405  caucvgprprlemaddq  6898  caucvgsrlemgt1  6971  lble  8025  supinfneg  8683  infsupneg  8684  fzrevral  9122  nfiseq  9438  fimaxre2  10109  nfsum1  10193  nfsum  10194  zsupcllemstep  10341  infssuzex  10345  infssuzcldc  10347  bezoutlemmain  10387  bezout  10400  prmind2  10502  oddpwdclemdvds  10548  oddpwdclemndvds  10549  elabf1  10591  elabf2  10592  elabg2  10595  bj-omssind  10730  bj-bdfindisg  10743  bj-nntrans  10746  bj-nnelirr  10748  bj-omtrans  10751  setindis  10762  bdsetindis  10764  bj-nn0sucALT  10773  bj-findis  10774  bj-findisg  10775  strcollnfALT  10781