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

Metamath Proof Explorer

Theorem nfmpt1

Description: Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008)

Ref Expression
Assertion nfmpt1 ⊢ Ⅎ _ x x ∈ A ⟼ B

Proof

Step Hyp Ref Expression
1 df-mpt ⊢ x ∈ A ⟼ B = x z | x ∈ A ∧ z = B
2 nfopab1 ⊢ Ⅎ _ x x z | x ∈ A ∧ z = B
3 1 2 nfcxfr ⊢ Ⅎ _ x x ∈ A ⟼ B