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

Metamath Proof Explorer

Theorem nfmpo1

Description: Bound-variable hypothesis builder for an operation in maps-to notation. (Contributed by NM, 27-Aug-2013)

Ref Expression
Assertion nfmpo1 ⊢ Ⅎ _ x x ∈ A , y ∈ B ⟼ C

Proof

Step Hyp Ref Expression
1 df-mpo ⊢ x ∈ A , y ∈ B ⟼ C = x y z | x ∈ A ∧ y ∈ B ∧ z = C
2 nfoprab1 ⊢ Ⅎ _ x x y z | x ∈ A ∧ y ∈ B ∧ z = C
3 1 2 nfcxfr ⊢ Ⅎ _ x x ∈ A , y ∈ B ⟼ C