Theorem nfcxfr 2487

Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypotheses

Ref	Expression
nfceqi.1	|- A = B
nfcxfr.2	|- F/_xB

Assertion

Ref	Expression
nfcxfr	|- F/_xA

Proof of Theorem nfcxfr

Step	Hyp	Ref	Expression
1		nfcxfr.2	. 2 |- F/_xB
2		nfceqi.1	. . 3 |- A = B
3	2	nfceqi 2486	. 2 |- ( F/_xA <-> F/_xB)
4	1, 3	mpbir 200	1 |- F/_xA

Syntax hints:   = wceq 1642   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-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-cleq 2346  df-clel 2349  df-nfc 2479

This theorem is referenced by:  nfrab1  2792  nfrab  2793  nfnin  3229  nfcompl  3230  nfin  3231  nfun  3232  nfdif  3233  nfsymdif  3234  nfpw  3734  nfpr  3774  nfsn  3785  nfuni  3898  nfint  3937  nfiun  3996  nfiin  3997  nfiu1  3998  nfii1  3999  nfopk  4069  nfiota1  4342  nfop  4605  nfopab  4628  nfopab1  4629  nfopab2  4630  nfxp  4811  nfco  4883  nfcnv  4892  nfres  4937  nfima  4954  nfrn  4964  nfdm  4965  nffv  5335  nfoprab1  5547  nfoprab2  5548  nfoprab3  5549  nfoprab  5550  ov3  5600  nfmpt  5672  nfmpt1  5673  nfmpt21  5674  nfmpt22  5675  nfmpt2  5676  fvmptss  5706  ov2gf  5712  fvmptf  5723