Theorem nfcxfr 2305

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

Syntax hints:   = wceq 1343  Ⅎwnfc 2295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-17 1514  ax-ial 1522  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-cleq 2158  df-clel 2161  df-nfc 2297

This theorem is referenced by:  nfrab1  2645  nfrabxy  2646  nfdif  3243  nfun  3278  nfin  3328  nfpw  3572  nfpr  3626  nfsn  3636  nfop  3774  nfuni  3795  nfint  3834  nfiunxy  3892  nfiinxy  3893  nfiunya  3894  nfiinya  3895  nfiu1  3896  nfii1  3897  nfopab  4050  nfopab1  4051  nfopab2  4052  nfmpt  4074  nfmpt1  4075  repizf2  4141  nfsuc  4386  nfxp  4631  nfco  4769  nfcnv  4783  nfdm  4848  nfrn  4849  nfres  4886  nfima  4954  nfiota1  5155  nffv  5496  fvmptss2  5561  fvmptssdm  5570  fvmptf  5578  ralrnmpt  5627  rexrnmpt  5628  f1ompt  5636  f1mpt  5739  fliftfun  5764  nfriota1  5805  riotaprop  5821  nfoprab1  5891  nfoprab2  5892  nfoprab3  5893  nfoprab  5894  nfmpo1  5909  nfmpo2  5910  nfmpo  5911  ovmpos  5965  ov2gf  5966  ovi3  5978  nfof  6055  nfofr  6056  nftpos  6247  nfrecs  6275  nffrec  6364  nfixpxy  6683  nfixp1  6684  xpcomco  6792  nfsup  6957  nfinf  6982  nfdju  7007  caucvgprprlemaddq  7649  nfseq  10390  nfsum1  11297  nfsum  11298  nfcprod1  11495  nfcprod  11496