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  2444  dvelimf  2446  nfmod2  2551  nfmodv  2552  nfeud2  2583  nfeudw  2584  nfeqd  2902  nfeld  2903  nfabdw  2913  nfabd  2914  nfned  3027  nfneld  3038  nfraldw  3275  nfrexdw  3276  nfrald  3337  nfrexd  3338  nfrmod  3392  nfreud  3393  nfsbc1d  3762  nfsbcdw  3765  nfsbcd  3768  nfbrd  5141  bj-dvelimdv  36824  bj-nfexd  37111  wl-sb8eut  37551  wl-sb8eutv  37552