Theorem nfcxfrd 2903

Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypotheses

Ref	Expression
nfcxfr.1	⊢ 𝐴 = 𝐵
nfcxfrd.2	⊢ (𝜑 → Ⅎ𝑥𝐵)

Assertion

Ref	Expression
nfcxfrd	⊢ (𝜑 → Ⅎ𝑥𝐴)

Proof of Theorem nfcxfrd

Step	Hyp	Ref	Expression
1		nfcxfrd.2	. 2 ⊢ (𝜑 → Ⅎ𝑥𝐵)
2		nfcxfr.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	nfceqi 2901	. 2 ⊢ (Ⅎ𝑥𝐴 ↔ Ⅎ𝑥𝐵)
4	1, 3	sylibr 233	1 ⊢ (𝜑 → Ⅎ𝑥𝐴)

Syntax hints:   → wi 4   = wceq 1542  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787  df-cleq 2725  df-clel 2811  df-nfc 2886

This theorem is referenced by:  nfcsb1d  3917  nfcsbd  3920  nfcsbw  3921  nfifd  4558  nfunid  4915  nfopabd  5217  nfiotadw  6499  nfiotad  6501  nfriotadw  7373  nfriotad  7377  nfovd  7438  nfttrcld  9705  nfnegd  11455  nfxnegd  44199  nfintd  47766  nfiund  47767  nfiundg  47768