Theorem nfxfrd 1850

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 1848	. 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓)
4	1, 3	sylibr 234	1 ⊢ (𝜒 → Ⅎ𝑥𝜑)

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

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

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

This theorem is referenced by:  nfand  1894  nf3and  1895  nfbid  1899  nfexd  2327  dvelimhw  2345  nfexd2  2448  dvelimf  2450  nfmod2  2555  nfmodv  2556  nfeud2  2587  nfeudw  2588  nfeqd  2913  nfeld  2914  nfabdw  2924  nfabd  2925  nfned  3041  nfneld  3052  nfraldw  3306  nfrexdw  3307  nfrald  3369  nfrexd  3370  nfreuwOLD  3422  nfrmod  3428  nfreud  3429  nfsbc1d  3808  nfsbcdw  3811  nfsbcd  3814  nfbrd  5193  bj-dvelimdv  36833  bj-nfexd  37120  wl-sb8eut  37558  wl-sb8eutv  37559