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

Metamath Proof Explorer

Theorem ssprss

Description: A pair as subset of a pair. (Contributed by AV, 26-Oct-2020)

Ref Expression
Assertion ssprss 
|- ( ( A e. V /\ B e. W ) -> ( { A , B } C_ { C , D } <-> ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) ) )

Proof

Step Hyp Ref Expression
1 prssg 
 |-  ( ( A e. V /\ B e. W ) -> ( ( A e. { C , D } /\ B e. { C , D } ) <-> { A , B } C_ { C , D } ) )
2 elprg 
 |-  ( A e. V -> ( A e. { C , D } <-> ( A = C \/ A = D ) ) )
3 elprg 
 |-  ( B e. W -> ( B e. { C , D } <-> ( B = C \/ B = D ) ) )
4 2 3 bi2anan9 
 |-  ( ( A e. V /\ B e. W ) -> ( ( A e. { C , D } /\ B e. { C , D } ) <-> ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) ) )
5 1 4 bitr3d 
 |-  ( ( A e. V /\ B e. W ) -> ( { A , B } C_ { C , D } <-> ( ( A = C \/ A = D ) /\ ( B = C \/ B = D ) ) ) )