Theorem nfcxfr 2389

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

Syntax hints:   = wceq 1402  Ⅎwnfc 2379

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-cleq 2231  df-clel 2234  df-nfc 2381

This theorem is referenced by:  nfrab1  2732  nfrabw  2733  nfdif  3350  nfun  3385  nfin  3437  nfpw  3701  nfpr  3755  nfsn  3765  nfop  3915  nfuni  3936  nfint  3975  nfiunxy  4033  nfiinxy  4034  nfiunya  4035  nfiinya  4036  nfiu1  4037  nfii1  4038  nfopab  4194  nfopab1  4195  nfopab2  4196  nfmpt  4218  nfmpt1  4219  repizf2  4294  nfsuc  4548  nfxp  4796  nfco  4940  nfcnv  4954  nfdm  5021  nfrn  5022  nfres  5060  nfima  5129  nfiota1  5334  nffv  5700  fvmptss2  5774  fvmptssdm  5784  fvmptf  5792  ralrnmpt  5841  rexrnmpt  5842  f1ompt  5850  f1mpt  5967  fliftfun  5992  nfriota1  6036  riotaprop  6054  nfoprab1  6127  nfoprab2  6128  nfoprab3  6129  nfoprab  6130  nfmpo1  6145  nfmpo2  6146  nfmpo  6147  ovmpos  6202  ov2gf  6203  ovi3  6216  nfof  6298  nfofr  6299  nftpos  6540  nfrecs  6568  nffrec  6657  nfixpxy  6989  nfixp1  6990  xpcomco  7114  nfsup  7322  nfinf  7347  nfdju  7372  caucvgprprlemaddq  8065  nfseq  10872  nfwrd  11311  nfsum1  12100  nfsum  12101  nfcprod1  12299  nfcprod  12300  ballotfilem7  13257  lgseisenlem2  16104  lfgrnloopen  16288