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 234	1 ⊢ (𝜒 → Ⅎ𝑥𝜑)

Syntax hints:   → wi 4   ↔ wb 206  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfand  1897  nf3and  1898  nfbid  1902  nfexd  2328  dvelimhw  2343  nfexd2  2445  dvelimf  2447  nfmod2  2552  nfmodv  2553  nfeud2  2584  nfeudw  2585  nfeqd  2903  nfeld  2904  nfabdw  2914  nfabd  2915  nfned  3028  nfneld  3039  nfraldw  3285  nfrexdw  3286  nfrald  3348  nfrexd  3349  nfrmod  3404  nfreud  3405  nfsbc1d  3774  nfsbcdw  3777  nfsbcd  3780  nfbrd  5156  bj-dvelimdv  36846  bj-nfexd  37133  wl-sb8eut  37573  wl-sb8eutv  37574