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

Metamath Proof Explorer

Theorem opelxp2

Description: The second member of an ordered pair of classes in a Cartesian product belongs to second Cartesian product argument. (Contributed by Mario Carneiro, 26-Apr-2015)

Ref Expression
Assertion opelxp2 ⊢ A B ∈ C × D → B ∈ D

Proof

Step Hyp Ref Expression
1 opelxp ⊢ A B ∈ C × D ↔ A ∈ C ∧ B ∈ D
2 1 simprbi ⊢ A B ∈ C × D → B ∈ D