Theorem nfcxfr 2383

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 2382	. 2 ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)
4	1, 3	mpbir 146	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:   = wceq 1398  Ⅎwnfc 2373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-cleq 2227  df-clel 2230  df-nfc 2375

This theorem is referenced by:  nfrab1  2726  nfrabw  2727  nfdif  3344  nfun  3379  nfin  3431  nfpw  3691  nfpr  3745  nfsn  3755  nfop  3905  nfuni  3926  nfint  3965  nfiunxy  4023  nfiinxy  4024  nfiunya  4025  nfiinya  4026  nfiu1  4027  nfii1  4028  nfopab  4184  nfopab1  4185  nfopab2  4186  nfmpt  4208  nfmpt1  4209  repizf2  4281  nfsuc  4535  nfxp  4783  nfco  4927  nfcnv  4941  nfdm  5008  nfrn  5009  nfres  5047  nfima  5116  nfiota1  5321  nffv  5687  fvmptss2  5759  fvmptssdm  5769  fvmptf  5777  ralrnmpt  5826  rexrnmpt  5827  f1ompt  5835  f1mpt  5952  fliftfun  5977  nfriota1  6021  riotaprop  6039  nfoprab1  6112  nfoprab2  6113  nfoprab3  6114  nfoprab  6115  nfmpo1  6130  nfmpo2  6131  nfmpo  6132  ovmpos  6187  ov2gf  6188  ovi3  6201  nfof  6283  nfofr  6284  nftpos  6525  nfrecs  6553  nffrec  6642  nfixpxy  6967  nfixp1  6968  xpcomco  7092  nfsup  7298  nfinf  7323  nfdju  7348  caucvgprprlemaddq  8041  nfseq  10848  nfwrd  11283  nfsum1  12072  nfsum  12073  nfcprod1  12271  nfcprod  12272  ballotfilem7  13229  lgseisenlem2  16076  lfgrnloopen  16260