Theorem nfxfrd 1857

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

Syntax hints:   → wi 4   ↔ wb 205  Ⅎwnf 1787

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

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-nf 1788

This theorem is referenced by:  nfand  1901  nf3and  1902  nfbid  1906  nfexd  2327  dvelimhw  2345  nfexd2  2446  dvelimf  2448  nfmod2  2558  nfmodv  2559  nfeud2  2590  nfeudw  2591  nfeqd  2916  nfeld  2917  nfabdw  2929  nfabdwOLD  2930  nfabd  2931  nfned  3045  nfneld  3056  nfraldw  3146  nfraldwOLD  3147  nfrald  3148  nfrexd  3235  nfrexdg  3236  nfreud  3298  nfrmod  3299  nfreuw  3300  nfsbc1d  3729  nfsbcdw  3732  nfsbcd  3735  nfbrd  5116  bj-dvelimdv  34962  bj-nfexd  35236  wl-sb8eut  35659