Theorem nfxfrd 1884

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

Syntax hints:   → wi 4   ↔ wb 209  Ⅎwnf 1813

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

This theorem depends on definitions:  df-bi 210  df-ex 1810  df-nf 1814

This theorem is referenced by:  nfand  1927  nf3and  1928  nfbid  1932  nfexd  2362  dvelimhw  2377  nfexd2  2478  dvelimf  2480  nfmod2  2586  nfmodv  2587  nfeud2  2618  nfeudw  2619  nfeqd  2935  nfeld  2936  nfabdw  2946  nfabd  2947  nfned  3062  nfneld  3073  nfraldw  3310  nfrexdw  3311  nfrald  3361  nfrexd  3362  nfrmod  3412  nfreud  3413  nfsbc1d  3763  nfsbcdw  3766  nfsbcd  3769  nfbrd  5158  nfchnd  18668  bj-dvelimdv  37467  bj-nfexd  37761  wl-sb8eut  38214  wl-sb8eutv  38215