Metamath Proof Explorer

Theorem opelopab3

Description: Ordered pair membership in an ordered pair class abstraction, with a reduced hypothesis. (Contributed by Jeff Madsen, 29-May-2011)

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

Proof

Step Hyp Ref Expression
1 opelopab3.1 ⊢ x = A → φ ↔ ψ
2 opelopab3.2 ⊢ y = B → ψ ↔ χ
3 opelopab3.3 ⊢ χ → A ∈ C
4 elopaelxp ⊢ A B ∈ x y | φ → A B ∈ V × V
5 opelxp1 ⊢ A B ∈ V × V → A ∈ V
6 4 5 syl ⊢ A B ∈ x y | φ → A ∈ V
7 6 anim1i ⊢ A B ∈ x y | φ ∧ B ∈ D → A ∈ V ∧ B ∈ D
8 7 ancoms ⊢ B ∈ D ∧ A B ∈ x y | φ → A ∈ V ∧ B ∈ D
9 3 elexd ⊢ χ → A ∈ V
10 9 anim1i ⊢ χ ∧ B ∈ D → A ∈ V ∧ B ∈ D
11 10 ancoms ⊢ B ∈ D ∧ χ → A ∈ V ∧ B ∈ D
12 1 2 opelopabg ⊢ A ∈ V ∧ B ∈ D → A B ∈ x y | φ ↔ χ
13 8 11 12 pm5.21nd ⊢ B ∈ D → A B ∈ x y | φ ↔ χ