Theorem nfcxfr 2369

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

Syntax hints:   = wceq 1395  Ⅎwnfc 2359

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-cleq 2222  df-clel 2225  df-nfc 2361

This theorem is referenced by:  nfrab1  2711  nfrabw  2712  nfdif  3326  nfun  3361  nfin  3411  nfpw  3663  nfpr  3717  nfsn  3727  nfop  3876  nfuni  3897  nfint  3936  nfiunxy  3994  nfiinxy  3995  nfiunya  3996  nfiinya  3997  nfiu1  3998  nfii1  3999  nfopab  4155  nfopab1  4156  nfopab2  4157  nfmpt  4179  nfmpt1  4180  repizf2  4250  nfsuc  4503  nfxp  4750  nfco  4893  nfcnv  4907  nfdm  4974  nfrn  4975  nfres  5013  nfima  5082  nfiota1  5286  nffv  5645  fvmptss2  5717  fvmptssdm  5727  fvmptf  5735  ralrnmpt  5785  rexrnmpt  5786  f1ompt  5794  f1mpt  5907  fliftfun  5932  nfriota1  5974  riotaprop  5992  nfoprab1  6065  nfoprab2  6066  nfoprab3  6067  nfoprab  6068  nfmpo1  6083  nfmpo2  6084  nfmpo  6085  ovmpos  6140  ov2gf  6141  ovi3  6154  nfof  6236  nfofr  6237  nftpos  6440  nfrecs  6468  nffrec  6557  nfixpxy  6881  nfixp1  6882  xpcomco  7005  nfsup  7182  nfinf  7207  nfdju  7232  caucvgprprlemaddq  7918  nfseq  10709  nfwrd  11132  nfsum1  11907  nfsum  11908  nfcprod1  12105  nfcprod  12106  lgseisenlem2  15790  lfgrnloopen  15972