Theorem nfxfrd 1887

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  nfand  1930  nf3and  1931  nfbid  1935  nfexd  2360  dvelimhw  2375  nfexd2  2476  dvelimf  2478  nfmod2  2584  nfmodv  2585  nfeud2  2616  nfeudw  2617  nfeqd  2933  nfeld  2934  nfabdw  2944  nfabd  2945  nfned  3060  nfneld  3071  nfraldw  3308  nfrexdw  3309  nfrald  3358  nfrexd  3359  nfrmod  3409  nfreud  3410  nfsbc1d  3757  nfsbcdw  3760  nfsbcd  3763  nfbrd  5151  nfchnd  18765  bj-dvelimdv  37733  bj-nfexd  38025  wl-sb8eut  38478  wl-sb8eutv  38479