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  2329  dvelimhw  2347  nfexd2  2451  dvelimf  2453  nfmod2  2558  nfmodv  2559  nfeud2  2590  nfeudw  2591  nfeqd  2916  nfeld  2917  nfabdw  2927  nfabd  2928  nfned  3044  nfneld  3055  nfraldw  3309  nfrexdw  3310  nfrald  3372  nfrexd  3373  nfreuwOLD  3426  nfrmod  3432  nfreud  3433  nfsbc1d  3806  nfsbcdw  3809  nfsbcd  3812  nfbrd  5189  bj-dvelimdv  36852  bj-nfexd  37139  wl-sb8eut  37579  wl-sb8eutv  37580