Theorem prssg 4028

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

Assertion

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

Proof of Theorem prssg

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

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   e. wcel 1756   u. cun 3326   C_ wss 3328   {csn 3877   {cpr 3879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-v 2974  df-un 3333  df-in 3335  df-ss 3342  df-sn 3878  df-pr 3880

This theorem is referenced by:  prssi  4029  prsspwg  4030  lspprss  17073  lspvadd  17177  topgele  18539  usgraedgprv  23295  usgraedgrnv  23296  usgraedg4  23305  2trllemH  23451  2trllemE  23452  dihmeetlem2N  34944