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 ) ) ) )