Theorem prssg

Description: A pair of elements of a class is a subset of the class. Theorem 7.5 of Quine p. 49. (Contributed by NM, 22-Mar-2006) (Proof shortened by Andrew Salmon, 29-Jun-2011)

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

Proof

Step	Hyp	Ref	Expression
1		snssg	|- ( A e. V -> ( A e. C <-> { A } C_ C ) )
2		snssg	|- ( B e. W -> ( B e. C <-> { B } C_ C ) )
3	1 2	bi2anan9	|- ( ( A e. V /\ B e. W ) -> ( ( A e. C /\ B e. C ) <-> ( { A } C_ C /\ { B } C_ C ) ) )
4		unss	|- ( ( { A } C_ C /\ { B } C_ C ) <-> ( { A } u. { B } ) C_ C )
5		df-pr	|- { A , B } = ( { A } u. { B } )
6	5	sseq1i	|- ( { A , B } C_ C <-> ( { A } u. { B } ) C_ C )
7	4 6	bitr4i	|- ( ( { A } C_ C /\ { B } C_ C ) <-> { A , B } C_ C )
8	3 7	bitrdi	|- ( ( A e. V /\ B e. W ) -> ( ( A e. C /\ B e. C ) <-> { A , B } C_ C ) )