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

Metamath Proof Explorer

Theorem nfmpt

Description: Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013)

Ref Expression
Hypotheses nfmpt.1 ⊢ Ⅎ _ x A
nfmpt.2 ⊢ Ⅎ _ x B
Assertion nfmpt ⊢ Ⅎ _ x y ∈ A ⟼ B

Proof

Step Hyp Ref Expression
1 nfmpt.1 ⊢ Ⅎ _ x A
2 nfmpt.2 ⊢ Ⅎ _ x B
3 df-mpt ⊢ y ∈ A ⟼ B = y z | y ∈ A ∧ z = B
4 1 nfcri ⊢ Ⅎ x y ∈ A
5 2 nfeq2 ⊢ Ⅎ x z = B
6 4 5 nfan ⊢ Ⅎ x y ∈ A ∧ z = B
7 6 nfopab ⊢ Ⅎ _ x y z | y ∈ A ∧ z = B
8 3 7 nfcxfr ⊢ Ⅎ _ x y ∈ A ⟼ B