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

Metamath Proof Explorer

Theorem opelopab2

Description: Ordered pair membership in an ordered pair class abstraction. (Contributed by NM, 14-Oct-2007) (Revised by Mario Carneiro, 19-Dec-2013)

Ref Expression
Hypotheses opelopab2.1 ⊢ x = A → φ ↔ ψ
opelopab2.2 ⊢ y = B → ψ ↔ χ
Assertion opelopab2 ⊢ A ∈ C ∧ B ∈ D → A B ∈ x y | x ∈ C ∧ y ∈ D ∧ φ ↔ χ

Proof

Step Hyp Ref Expression
1 opelopab2.1 ⊢ x = A → φ ↔ ψ
2 opelopab2.2 ⊢ y = B → ψ ↔ χ
3 1 2 sylan9bb ⊢ x = A ∧ y = B → φ ↔ χ
4 3 opelopab2a ⊢ A ∈ C ∧ B ∈ D → A B ∈ x y | x ∈ C ∧ y ∈ D ∧ φ ↔ χ