Theorem nfcxfr 2336

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

Syntax hints:   = wceq 1364  Ⅎwnfc 2326

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-cleq 2189  df-clel 2192  df-nfc 2328

This theorem is referenced by:  nfrab1  2677  nfrabw  2678  nfdif  3285  nfun  3320  nfin  3370  nfpw  3619  nfpr  3673  nfsn  3683  nfop  3825  nfuni  3846  nfint  3885  nfiunxy  3943  nfiinxy  3944  nfiunya  3945  nfiinya  3946  nfiu1  3947  nfii1  3948  nfopab  4102  nfopab1  4103  nfopab2  4104  nfmpt  4126  nfmpt1  4127  repizf2  4196  nfsuc  4444  nfxp  4691  nfco  4832  nfcnv  4846  nfdm  4911  nfrn  4912  nfres  4949  nfima  5018  nfiota1  5222  nffv  5571  fvmptss2  5639  fvmptssdm  5649  fvmptf  5657  ralrnmpt  5707  rexrnmpt  5708  f1ompt  5716  f1mpt  5821  fliftfun  5846  nfriota1  5888  riotaprop  5904  nfoprab1  5975  nfoprab2  5976  nfoprab3  5977  nfoprab  5978  nfmpo1  5993  nfmpo2  5994  nfmpo  5995  ovmpos  6050  ov2gf  6051  ovi3  6064  nfof  6145  nfofr  6146  nftpos  6346  nfrecs  6374  nffrec  6463  nfixpxy  6785  nfixp1  6786  xpcomco  6894  nfsup  7067  nfinf  7092  nfdju  7117  caucvgprprlemaddq  7792  nfseq  10566  nfwrd  10980  nfsum1  11538  nfsum  11539  nfcprod1  11736  nfcprod  11737  lgseisenlem2  15396