Theorem nfcv 2489

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	|- F/_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 1619	. 2 |- F/x y e. A
2	1	nfci 2479	1 |- F/_xA

Syntax hints:   e. wcel 1710   F/_wnfc 2476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-17 1616

This theorem depends on definitions:  df-bi 177  df-nf 1545  df-nfc 2478

This theorem is referenced by:  nfcvd  2490  nfel  2497  nfeq1  2498  nfel1  2499  nfeq2  2500  nfel2  2501  nfcvf  2511  r2al  2651  r2ex  2652  nfra2  2668  r19.12  2727  ralcom  2771  rexcom  2772  raleq  2807  rexeq  2808  reueq1  2809  rmoeq1  2810  cbvral  2831  cbvrex  2832  rabeq  2853  cbvrabv  2858  vtoclg  2914  vtocl2g  2918  vtoclga  2920  vtocl2ga  2922  vtocl3ga  2924  spcimdv  2936  spcgv  2939  spcegv  2940  rspct  2948  rspc  2949  rspce  2950  rspc2  2960  ceqsexg  2970  elabgt  2982  elabf  2984  elabg  2986  elab3g  2991  elrab  2994  mob  3018  2rmorex  3040  nfsbc1v  3065  elrabsf  3084  sbcralt  3118  sbcralg  3120  sbcrexg  3121  sbcreug  3122  cbvcsbv  3141  csbexg  3146  csbconstg  3150  nfcsb1v  3168  csbnestg  3186  cbvralcsf  3198  cbvreucsf  3200  cbvrabcsf  3201  cbvralv2  3202  cbvrexv2  3203  n0f  3558  n0  3559  raaan  3657  nfpw  3733  cbviunv  4005  cbviinv  4006  ssiun2s  4010  iunab  4012  ssiinf  4015  ssiin  4016  iinab  4027  opelopabf  4711  opeliunxp  4820  opeliunxp2  4822  ralxpf  4827  nfco  4882  nfcnv  4891  dfdmf  4905  nfres  4936  nfima  4953  dfrnf  4962  nfrn  4963  dffun6f  5123  dffun6  5124  nffun  5130  nffv  5334  funfv2f  5377  eqfnfv2f  5396  ffnfvf  5428  funiunfvf  5468  dff13f  5472  nfiso  5487  ov3  5599  mpt2eq123  5661  cbvmptv  5677  cbvmpt2x  5678  cbvmpt2  5679  cbvmpt2v  5680  fvmpts  5701  fvmpt2i  5703  fvmptss  5705  ov2gf  5711  fvmptex  5721  fvmptnf  5723  fvmptn  5724  fmpt2x  5730  eqerlem  5960