Theorem prssg 4112

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 4090	. . 3 |- ( A e. V -> ( A e. C <-> { A } C_ C ) )
2		snssg 4090	. . 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 3605	. . 3 |- ( ( { A } C_ C /\ { B } C_ C ) <-> ( { A } u. { B } ) C_ C )
5		df-pr 3960	. . . 4 |- { A , B } = ( { A } u. { B } )
6	5	sseq1i 3454	. . 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 367   e. wcel 1836   u. cun 3400   C_ wss 3402   {csn 3957   {cpr 3959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-v 3049  df-un 3407  df-in 3409  df-ss 3416  df-sn 3958  df-pr 3960

This theorem is referenced by:  prssi  4113  prsspwg  4114  lspprss  17770  lspvadd  17874  topgele  19539  usgraedgprv  24518  usgraedgrnv  24519  usgraedg4  24529  2trllemH  24696  2trllemE  24697  fourierdlem20  32110  fourierdlem50  32140  fourierdlem54  32144  fourierdlem64  32154  fourierdlem76  32166  prelpw  32655  dihmeetlem2N  37474