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

Metamath Proof Explorer

Theorem elmpocl

Description: If a two-parameter class is not empty, constrain the implicit pair. (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Hypothesis elmpocl.f 
|- F = ( x e. A , y e. B |-> C )
Assertion elmpocl 
|- ( X e. ( S F T ) -> ( S e. A /\ T e. B ) )

Proof

Step Hyp Ref Expression
1 elmpocl.f 
 |-  F = ( x e. A , y e. B |-> C )
2 df-mpo 
 |-  ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
3 1 2 eqtri 
 |-  F = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
4 3 dmeqi 
 |-  dom F = dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
5 dmoprabss 
 |-  dom { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } C_ ( A X. B )
6 4 5 eqsstri 
 |-  dom F C_ ( A X. B )
7 elfvdm 
 |-  ( X e. ( F ` <. S , T >. ) -> <. S , T >. e. dom F )
8 df-ov 
 |-  ( S F T ) = ( F ` <. S , T >. )
9 7 8 eleq2s 
 |-  ( X e. ( S F T ) -> <. S , T >. e. dom F )
10 6 9 sselid 
 |-  ( X e. ( S F T ) -> <. S , T >. e. ( A X. B ) )
11 opelxp 
 |-  ( <. S , T >. e. ( A X. B ) <-> ( S e. A /\ T e. B ) )
12 10 11 sylib 
 |-  ( X e. ( S F T ) -> ( S e. A /\ T e. B ) )