Theorem nfcxfr 2486

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 2485	. 2 |- ( F/_xA <-> F/_xB)
4	1, 3	mpbir 200	1 |- F/_xA

Syntax hints:   = wceq 1642   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-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 2478

This theorem is referenced by:  nfrab1  2791  nfrab  2792  nfnin  3228  nfcompl  3229  nfin  3230  nfun  3231  nfdif  3232  nfsymdif  3233  nfpw  3733  nfpr  3773  nfsn  3784  nfuni  3897  nfint  3936  nfiun  3995  nfiin  3996  nfiu1  3997  nfii1  3998  nfopk  4068  nfiota1  4341  nfop  4604  nfopab  4627  nfopab1  4628  nfopab2  4629  nfxp  4810  nfco  4882  nfcnv  4891  nfres  4936  nfima  4953  nfrn  4963  nfdm  4964  nffv  5334  nfoprab1  5546  nfoprab2  5547  nfoprab3  5548  nfoprab  5549  ov3  5599  nfmpt  5671  nfmpt1  5672  nfmpt21  5673  nfmpt22  5674  nfmpt2  5675  fvmptss  5705  ov2gf  5711  fvmptf  5722