MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prssg Structured version   Unicode version

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
StepHypRef 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 ) )
31, 2bi2anan9 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 } )
65sseq1i 3454 . . 3  |-  ( { A ,  B }  C_  C  <->  ( { A }  u.  { B } )  C_  C
)
74, 6bitr4i 252 . 2  |-  ( ( { A }  C_  C  /\  { B }  C_  C )  <->  { A ,  B }  C_  C
)
83, 7syl6bb 261 1  |-  ( ( A  e.  V  /\  B  e.  W )  ->  ( ( A  e.  C  /\  B  e.  C )  <->  { A ,  B }  C_  C
) )
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator