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 1786

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

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfand  1901  nf3and  1902  nfbid  1906  nfexd  2323  dvelimhw  2342  nfexd2  2446  dvelimf  2448  nfmod2  2553  nfmodv  2554  nfeud2  2585  nfeudw  2586  nfeqd  2914  nfeld  2915  nfabdw  2927  nfabdwOLD  2928  nfabd  2929  nfned  3045  nfneld  3056  nfraldw  3307  nfrexdw  3308  nfraldwOLD  3319  nfrald  3369  nfrexd  3370  nfreuwOLD  3423  nfrmod  3429  nfreud  3430  nfsbc1d  3796  nfsbcdw  3799  nfsbcd  3802  nfbrd  5195  bj-dvelimdv  35778  bj-nfexd  36067  wl-sb8eut  36490