Theorem nfcxfr 2347

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

Syntax hints:   = wceq 1373  Ⅎwnfc 2337

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-cleq 2200  df-clel 2203  df-nfc 2339

This theorem is referenced by:  nfrab1  2688  nfrabw  2689  nfdif  3302  nfun  3337  nfin  3387  nfpw  3639  nfpr  3693  nfsn  3703  nfop  3849  nfuni  3870  nfint  3909  nfiunxy  3967  nfiinxy  3968  nfiunya  3969  nfiinya  3970  nfiu1  3971  nfii1  3972  nfopab  4128  nfopab1  4129  nfopab2  4130  nfmpt  4152  nfmpt1  4153  repizf2  4222  nfsuc  4473  nfxp  4720  nfco  4861  nfcnv  4875  nfdm  4941  nfrn  4942  nfres  4980  nfima  5049  nfiota1  5253  nffv  5609  fvmptss2  5677  fvmptssdm  5687  fvmptf  5695  ralrnmpt  5745  rexrnmpt  5746  f1ompt  5754  f1mpt  5863  fliftfun  5888  nfriota1  5930  riotaprop  5946  nfoprab1  6017  nfoprab2  6018  nfoprab3  6019  nfoprab  6020  nfmpo1  6035  nfmpo2  6036  nfmpo  6037  ovmpos  6092  ov2gf  6093  ovi3  6106  nfof  6187  nfofr  6188  nftpos  6388  nfrecs  6416  nffrec  6505  nfixpxy  6827  nfixp1  6828  xpcomco  6946  nfsup  7120  nfinf  7145  nfdju  7170  caucvgprprlemaddq  7856  nfseq  10639  nfwrd  11059  nfsum1  11782  nfsum  11783  nfcprod1  11980  nfcprod  11981  lgseisenlem2  15663  lfgrnloopen  15839