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 ⊢ Ⅎ x ψ
Assertion nfxfr ⊢ Ⅎ x φ

Proof

Step Hyp Ref Expression
1 nfbii.1 ⊢ φ ↔ ψ
2 nfxfr.2 ⊢ Ⅎ x ψ
3 1 nfbii ⊢ Ⅎ x φ ↔ Ⅎ x ψ
4 2 3 mpbir ⊢ Ⅎ x φ