Theorem nfcxfr 2381

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

Syntax hints:   = wceq 1398  Ⅎwnfc 2371

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-cleq 2225  df-clel 2228  df-nfc 2373

This theorem is referenced by:  nfrab1  2724  nfrabw  2725  nfdif  3340  nfun  3375  nfin  3427  nfpw  3685  nfpr  3739  nfsn  3749  nfop  3899  nfuni  3920  nfint  3959  nfiunxy  4017  nfiinxy  4018  nfiunya  4019  nfiinya  4020  nfiu1  4021  nfii1  4022  nfopab  4178  nfopab1  4179  nfopab2  4180  nfmpt  4202  nfmpt1  4203  repizf2  4275  nfsuc  4529  nfxp  4776  nfco  4920  nfcnv  4934  nfdm  5001  nfrn  5002  nfres  5040  nfima  5109  nfiota1  5314  nffv  5680  fvmptss2  5752  fvmptssdm  5762  fvmptf  5770  ralrnmpt  5819  rexrnmpt  5820  f1ompt  5828  f1mpt  5944  fliftfun  5969  nfriota1  6011  riotaprop  6029  nfoprab1  6102  nfoprab2  6103  nfoprab3  6104  nfoprab  6105  nfmpo1  6120  nfmpo2  6121  nfmpo  6122  ovmpos  6177  ov2gf  6178  ovi3  6191  nfof  6272  nfofr  6273  nftpos  6510  nfrecs  6538  nffrec  6627  nfixpxy  6952  nfixp1  6953  xpcomco  7077  nfsup  7283  nfinf  7308  nfdju  7333  caucvgprprlemaddq  8023  nfseq  10819  nfwrd  11253  nfsum1  12041  nfsum  12042  nfcprod1  12240  nfcprod  12241  lgseisenlem2  15944  lfgrnloopen  16128