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 ⊢ Ⅎ𝑥𝐴

This proof depends on syntax axioms:   = wceq 1402  Ⅎwnfc 2379

This proof depends on 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 proof depends on definitions:  df-bi 117  df-nf 1514  df-cleq 2231  df-clel 2234  df-nfc 2381

This theorem is used by:  nfrab1  2732  nfrabw  2733  nfdif  3350  nfun  3385  nfin  3437  nfpw  3705  nfpr  3759  nfsn  3769  nfop  3920  nfuni  3941  nfint  3980  nfiunxy  4038  nfiinxy  4039  nfiunya  4040  nfiinya  4041  nfiu1  4042  nfii1  4043  nfopab  4199  nfopab1  4200  nfopab2  4201  nfmpt  4223  nfmpt1  4224  repizf2  4299  nfsuc  4553  nfxp  4801  nfco  4945  nfcnv  4959  nfdm  5026  nfrn  5027  nfres  5065  nfima  5134  nfiota1  5339  nffv  5705  fvmptss2  5780  fvmptssdm  5790  fvmptf  5798  ralrnmpt  5850  rexrnmpt  5851  f1ompt  5859  f1mpt  5977  fliftfun  6002  nfriota1  6046  riotaprop  6064  nfoprab1  6137  nfoprab2  6138  nfoprab3  6139  nfoprab  6140  nfmpo1  6155  nfmpo2  6156  nfmpo  6157  ovmpos  6212  ov2gf  6213  ovi3  6226  nfof  6308  nfofr  6309  nftpos  6550  nfrecs  6578  nffrec  6667  nfixpxy  6999  nfixp1  7000  xpcomco  7124  nfsup  7332  nfinf  7357  nfdju  7382  caucvgprprlemaddq  8075  nfseq  10894  nfwrd  11333  nfsum1  12122  nfsum  12123  nfcprod1  12321  nfcprod  12322  ballotfilem7  13279  lgseisenlem2  16190  lfgrnloopen  16374