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

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
StepHypRef 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 ) )
31, 2bi2anan9 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 } )
65sseq1i 3468 . . 3  |-  ( { A ,  B }  C_  C  <->  ( { A }  u.  { B } )  C_  C
)
74, 6bitr4i 260 . 2  |-  ( ( { A }  C_  C  /\  { B }  C_  C )  <->  { A ,  B }  C_  C
)
83, 7syl6bb 269 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 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
  Copyright terms: Public domain W3C validator