Theorem prssg 4140

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 4118	. . 3 |- ( A e. V -> ( A e. C <-> { A } C_ C ) )
2		snssg 4118	. . 3 |- ( B e. W -> ( B e. C <-> { B } C_ C ) )
3	1, 2	bi2anan9 889	. 2 |- ( ( A e. V /\ B e. W ) -> ( ( A e. C /\ B e. C ) <-> ( { A } C_ C /\ { B } C_ C ) ) )
4		unss 3620	. . 3 |- ( ( { A } C_ C /\ { B } C_ C ) <-> ( { A } u. { B } ) C_ C )
5		df-pr 3983	. . . 4 |- { A , B } = ( { A } u. { B } )
6	5	sseq1i 3468	. . 3 |- ( { A , B } C_ C <-> ( { A } u. { B } ) C_ C )
7	4, 6	bitr4i 260	. 2 |- ( ( { A } C_ C /\ { B } C_ C ) <-> { A , B } C_ C )
8	3, 7	syl6bb 269	1 |- ( ( A e. V /\ B e. W ) -> ( ( A e. C /\ B e. C ) <-> { A , B } C_ C ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   e. wcel 1898   u. cun 3414   C_ wss 3416   {csn 3980   {cpr 3982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-un 3421  df-in 3423  df-ss 3430  df-sn 3981  df-pr 3983

This theorem is referenced by:  prssi  4141  prsspwg  4142  lspprss  18264  lspvadd  18368  topgele  19998  usgraedgprv  25152  usgraedgrnv  25153  usgraedg4  25163  2trllemH  25331  2trllemE  25332  dihmeetlem2N  34912  prssd  37422  fourierdlem20  38027  fourierdlem50  38058  fourierdlem54  38062  fourierdlem64  38072  fourierdlem76  38084  omeunle  38375  prelpw  39033  ssprss  39041  umgredgprv  39243  usgredgprvALT  39326  dfnbgr2  39457  nbuhgr  39461  uhgrnbgr0nb  39472  11wlkdlem2  39853  21wlkdlem6  39880