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

Metamath Proof Explorer

Theorem opabssxpd

Description: An ordered-pair class abstraction is a subset of a Cartesian product. Formerly part of proof for opabex2 . (Contributed by AV, 26-Nov-2021)

Ref Expression
Hypotheses opabssxpd.x 
|- ( ( ph /\ ps ) -> x e. A )
opabssxpd.y 
|- ( ( ph /\ ps ) -> y e. B )
Assertion opabssxpd 
|- ( ph -> { <. x , y >. | ps } C_ ( A X. B ) )

Proof

Step Hyp Ref Expression
1 opabssxpd.x 
 |-  ( ( ph /\ ps ) -> x e. A )
2 opabssxpd.y 
 |-  ( ( ph /\ ps ) -> y e. B )
3 df-opab 
 |-  { <. x , y >. | ps } = { z | E. x E. y ( z = <. x , y >. /\ ps ) }
4 simprl 
 |-  ( ( ph /\ ( z = <. x , y >. /\ ps ) ) -> z = <. x , y >. )
5 1 2 opelxpd 
 |-  ( ( ph /\ ps ) -> <. x , y >. e. ( A X. B ) )
6 5 adantrl 
 |-  ( ( ph /\ ( z = <. x , y >. /\ ps ) ) -> <. x , y >. e. ( A X. B ) )
7 4 6 eqeltrd 
 |-  ( ( ph /\ ( z = <. x , y >. /\ ps ) ) -> z e. ( A X. B ) )
8 7 ex 
 |-  ( ph -> ( ( z = <. x , y >. /\ ps ) -> z e. ( A X. B ) ) )
9 8 exlimdvv 
 |-  ( ph -> ( E. x E. y ( z = <. x , y >. /\ ps ) -> z e. ( A X. B ) ) )
10 9 abssdv 
 |-  ( ph -> { z | E. x E. y ( z = <. x , y >. /\ ps ) } C_ ( A X. B ) )
11 3 10 eqsstrid 
 |-  ( ph -> { <. x , y >. | ps } C_ ( A X. B ) )