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  4200  nfopab1  4201  nfopab2  4202  nfmpt  4225  nfmpt1  4226  repizf2  4301  nfsuc  4555  nfxp  4803  nfco  4947  nfcnv  4961  nfdm  5028  nfrn  5029  nfres  5067  nfima  5137  nfiota1  5342  nffv  5708  fvmptss2  5783  fvmptssdm  5793  fvmptf  5801  ralrnmpt  5853  rexrnmpt  5854  f1ompt  5862  f1mpt  5980  fliftfun  6005  nfriota1  6049  riotaprop  6067  nfoprab1  6140  nfoprab2  6141  nfoprab3  6142  nfoprab  6143  nfmpo1  6158  nfmpo2  6159  nfmpo  6160  ovmpos  6215  ov2gf  6216  ovi3  6229  nfof  6312  nfofr  6313  nftpos  6554  nfrecs  6582  nffrec  6671  nfixpxy  7003  nfixp1  7004  xpcomco  7128  nfsup  7338  nfinf  7363  nfdju  7388  caucvgprprlemaddq  8081  nfseq  10915  nfwrd  11355  nfsum1  12147  nfsum  12148  nfcprod1  12346  nfcprod  12347  ballotfilem7  13337  lgseisenlem2  16395  lfgrnloopen  16579