Theorem nfcv 2490

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 2480	1 |- F/_xA

Syntax hints:   e. wcel 1710   F/_wnfc 2477

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 2479

This theorem is referenced by:  nfcvd  2491  nfel  2498  nfeq1  2499  nfel1  2500  nfeq2  2501  nfel2  2502  nfcvf  2512  r2al  2652  r2ex  2653  nfra2  2669  r19.12  2728  ralcom  2772  rexcom  2773  raleq  2808  rexeq  2809  reueq1  2810  rmoeq1  2811  cbvral  2832  cbvrex  2833  rabeq  2854  cbvrabv  2859  vtoclg  2915  vtocl2g  2919  vtoclga  2921  vtocl2ga  2923  vtocl3ga  2925  spcimdv  2937  spcgv  2940  spcegv  2941  rspct  2949  rspc  2950  rspce  2951  rspc2  2961  ceqsexg  2971  elabgt  2983  elabf  2985  elabg  2987  elab3g  2992  elrab  2995  mob  3019  2rmorex  3041  nfsbc1v  3066  elrabsf  3085  sbcralt  3119  sbcralg  3121  sbcrexg  3122  sbcreug  3123  cbvcsbv  3142  csbexg  3147  csbconstg  3151  nfcsb1v  3169  csbnestg  3187  cbvralcsf  3199  cbvreucsf  3201  cbvrabcsf  3202  cbvralv2  3203  cbvrexv2  3204  n0f  3559  n0  3560  raaan  3658  nfpw  3734  cbviunv  4006  cbviinv  4007  ssiun2s  4011  iunab  4013  ssiinf  4016  ssiin  4017  iinab  4028  opelopabf  4712  opeliunxp  4821  opeliunxp2  4823  ralxpf  4828  nfco  4883  nfcnv  4892  dfdmf  4906  nfres  4937  nfima  4954  dfrnf  4963  nfrn  4964  dffun6f  5124  dffun6  5125  nffun  5131  nffv  5335  funfv2f  5378  eqfnfv2f  5397  ffnfvf  5429  funiunfvf  5469  dff13f  5473  nfiso  5488  ov3  5600  mpt2eq123  5662  cbvmptv  5678  cbvmpt2x  5679  cbvmpt2  5680  cbvmpt2v  5681  fvmpts  5702  fvmpt2i  5704  fvmptss  5706  ov2gf  5712  fvmptex  5722  fvmptnf  5724  fvmptn  5725  fmpt2x  5731  eqerlem  5961