Theorem prssg 4182

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 4160	. . 3 |- ( A e. V -> ( A e. C <-> { A } C_ C ) )
2		snssg 4160	. . 3 |- ( B e. W -> ( B e. C <-> { B } C_ C ) )
3	1, 2	bi2anan9 871	. 2 |- ( ( A e. V /\ B e. W ) -> ( ( A e. C /\ B e. C ) <-> ( { A } C_ C /\ { B } C_ C ) ) )
4		unss 3678	. . 3 |- ( ( { A } C_ C /\ { B } C_ C ) <-> ( { A } u. { B } ) C_ C )
5		df-pr 4030	. . . 4 |- { A , B } = ( { A } u. { B } )
6	5	sseq1i 3528	. . 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 1767   u. cun 3474   C_ wss 3476   {csn 4027   {cpr 4029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-in 3483  df-ss 3490  df-sn 4028  df-pr 4030

This theorem is referenced by:  prssi  4183  prsspwg  4184  lspprss  17418  lspvadd  17522  topgele  19199  usgraedgprv  24049  usgraedgrnv  24050  usgraedg4  24060  2trllemH  24227  2trllemE  24228  fourierdlem20  31427  fourierdlem50  31457  fourierdlem54  31461  fourierdlem64  31471  fourierdlem76  31483  fourierdlem93  31500  prelpw  31766  dihmeetlem2N  36096