This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfxfr

Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 11-Aug-2016)

Ref Expression
Hypotheses nfbii.1 ⊢ ( 𝜑 ↔ 𝜓 )
nfxfr.2 ⊢ Ⅎ 𝑥 𝜓
Assertion nfxfr Ⅎ 𝑥 𝜑

Proof

Step Hyp Ref Expression
1 nfbii.1 ⊢ ( 𝜑 ↔ 𝜓 )
2 nfxfr.2 ⊢ Ⅎ 𝑥 𝜓
3 1 nfbii ⊢ ( Ⅎ 𝑥 𝜑 ↔ Ⅎ 𝑥 𝜓 )
4 2 3 mpbir ⊢ Ⅎ 𝑥 𝜑