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

Theorem prss 3769
Description: A pair of elements of a class is a subset of the class. Theorem 7.5 of [Quine] p. 49. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
Hypotheses
Ref Expression
prss.1  |-  A  e. 
_V
prss.2  |-  B  e. 
_V
Assertion
Ref Expression
prss  |-  ( ( A  e.  C  /\  B  e.  C )  <->  { A ,  B }  C_  C )

Proof of Theorem prss
StepHypRef Expression
1 unss 3349 . 2  |-  ( ( { A }  C_  C  /\  { B }  C_  C )  <->  ( { A }  u.  { B } )  C_  C
)
2 prss.1 . . . 4  |-  A  e. 
_V
32snss 3748 . . 3  |-  ( A  e.  C  <->  { A }  C_  C )
4 prss.2 . . . 4  |-  B  e. 
_V
54snss 3748 . . 3  |-  ( B  e.  C  <->  { B }  C_  C )
63, 5anbi12i 678 . 2  |-  ( ( A  e.  C  /\  B  e.  C )  <->  ( { A }  C_  C  /\  { B }  C_  C ) )
7 df-pr 3647 . . 3  |-  { A ,  B }  =  ( { A }  u.  { B } )
87sseq1i 3202 . 2  |-  ( { A ,  B }  C_  C  <->  ( { A }  u.  { B } )  C_  C
)
91, 6, 83bitr4i 268 1  |-  ( ( A  e.  C  /\  B  e.  C )  <->  { A ,  B }  C_  C )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    e. wcel 1684   _Vcvv 2788    u. cun 3150    C_ wss 3152   {csn 3640   {cpr 3641
This theorem is referenced by:  tpss  3779  prsspw  3785  uniintsn  3899  pwssun  4299  xpsspwOLD  4798  dffv2  5592  fiint  7133  wunex2  8360  hashfun  11389  prdsle  13361  prdsless  13362  prdsleval  13376  pwsle  13391  acsfn2  13565  clatl  14220  ipoval  14257  ipolerval  14259  eqgfval  14665  eqgval  14666  gaorb  14761  efgcpbllema  15063  frgpuplem  15081  drngnidl  15981  drnglpir  16005  ltbval  16213  ltbwe  16214  opsrle  16217  opsrtoslem1  16225  thlle  16597  isphtpc  18492  shincli  21941  chincli  22039  altxpsspw  24511  axlowdimlem4  24573  toplat  25290  pgapspf2  26053  frgra2v  28177  frgra3vlem1  28178  frgra3vlem2  28179
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-in 3159  df-ss 3166  df-sn 3646  df-pr 3647
  Copyright terms: Public domain W3C validator