Theorem nfxfrd 1854

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

Hypotheses

Ref	Expression
nfbii.1	⊢ (𝜑 ↔ 𝜓)
nfxfrd.2	⊢ (𝜒 → Ⅎ𝑥𝜓)

Assertion

Ref	Expression
nfxfrd	⊢ (𝜒 → Ⅎ𝑥𝜑)

Proof of Theorem nfxfrd

Step	Hyp	Ref	Expression
1		nfxfrd.2	. 2 ⊢ (𝜒 → Ⅎ𝑥𝜓)
2		nfbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	nfbii 1852	. 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
4	1, 3	sylibr 236	1 ⊢ (𝜒 → Ⅎ𝑥𝜑)

Syntax hints:   → wi 4   ↔ wb 208  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 209  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfand  1898  nf3and  1899  nfbid  1903  nfexd  2348  dvelimhw  2366  nfexd2  2468  dvelimf  2470  nfmod2  2642  nfmodv  2643  nfeud2  2676  nfeudw  2677  nfeqd  2988  nfeld  2989  nfabdw  3000  nfabd  3001  nfabd2OLD  3003  nfned  3120  nfneld  3131  nfraldw  3223  nfrald  3224  nfrexd  3307  nfrexdg  3308  nfreud  3372  nfrmod  3373  nfreuw  3374  nfsbc1d  3790  nfsbcdw  3793  nfsbcd  3796  nfbrd  5112  bj-dvelimdv  34175  bj-nfexd  34433  wl-sb8eut  34828