Theorem nfcxfr 2279

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	⊢ 𝐴 = 𝐵
nfcxfr.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfcxfr	⊢ Ⅎ𝑥𝐴

Proof of Theorem nfcxfr

Step	Hyp	Ref	Expression
1		nfcxfr.2	. 2 ⊢ Ⅎ𝑥𝐵
2		nfceqi.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	nfceqi 2278	. 2 ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)
4	1, 3	mpbir 145	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:   = wceq 1332  Ⅎwnfc 2269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-cleq 2133  df-clel 2136  df-nfc 2271

This theorem is referenced by:  nfrab1  2613  nfrabxy  2614  nfdif  3202  nfun  3237  nfin  3287  nfpw  3528  nfpr  3581  nfsn  3591  nfop  3729  nfuni  3750  nfint  3789  nfiunxy  3847  nfiinxy  3848  nfiunya  3849  nfiinya  3850  nfiu1  3851  nfii1  3852  nfopab  4004  nfopab1  4005  nfopab2  4006  nfmpt  4028  nfmpt1  4029  repizf2  4094  nfsuc  4338  nfxp  4574  nfco  4712  nfcnv  4726  nfdm  4791  nfrn  4792  nfres  4829  nfima  4897  nfiota1  5098  nffv  5439  fvmptss2  5504  fvmptssdm  5513  fvmptf  5521  ralrnmpt  5570  rexrnmpt  5571  f1ompt  5579  f1mpt  5680  fliftfun  5705  nfriota1  5745  riotaprop  5761  nfoprab1  5828  nfoprab2  5829  nfoprab3  5830  nfoprab  5831  nfmpo1  5846  nfmpo2  5847  nfmpo  5848  ovmpos  5902  ov2gf  5903  ovi3  5915  nfof  5995  nfofr  5996  nftpos  6184  nfrecs  6212  nffrec  6301  nfixpxy  6619  nfixp1  6620  xpcomco  6728  nfsup  6887  nfinf  6912  nfdju  6935  caucvgprprlemaddq  7540  nfseq  10259  nfsum1  11157  nfsum  11158  nfcprod1  11355  nfcprod  11356