Theorem nfcxfr 2232

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

Syntax hints:   = wceq 1296  Ⅎwnfc 2222

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-4 1452  ax-17 1471  ax-ial 1479  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-nf 1402  df-cleq 2088  df-clel 2091  df-nfc 2224

This theorem is referenced by:  nfrab1  2560  nfrabxy  2561  nfdif  3136  nfun  3171  nfin  3221  nfpw  3462  nfpr  3512  nfsn  3522  nfop  3660  nfuni  3681  nfint  3720  nfiunxy  3778  nfiinxy  3779  nfiunya  3780  nfiinya  3781  nfiu1  3782  nfii1  3783  nfopab  3928  nfopab1  3929  nfopab2  3930  nfmpt  3952  nfmpt1  3953  repizf2  4018  nfsuc  4259  nfxp  4494  nfco  4632  nfcnv  4646  nfdm  4711  nfrn  4712  nfres  4747  nfima  4815  nfiota1  5016  nffv  5350  fvmptss2  5414  fvmptssdm  5423  fvmptf  5431  ralrnmpt  5480  rexrnmpt  5481  f1ompt  5489  f1mpt  5588  fliftfun  5613  nfriota1  5653  riotaprop  5669  nfoprab1  5736  nfoprab2  5737  nfoprab3  5738  nfoprab  5739  nfmpt21  5753  nfmpt22  5754  nfmpt2  5755  ovmpt2s  5806  ov2gf  5807  ovi3  5819  nfof  5899  nfofr  5900  nftpos  6082  nfrecs  6110  nffrec  6199  nfixpxy  6514  nfixp1  6515  xpcomco  6622  nfsup  6767  nfinf  6792  nfdju  6815  caucvgprprlemaddq  7364  nfseq  10010  nfsum1  10899  nfsum  10900