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

Theorem prss 3771
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 3351 . 2  |-  ( ( { A }  C_  C  /\  { B }  C_  C )  <->  ( { A }  u.  { B } )  C_  C
)
2 prss.1 . . . 4  |-  A  e. 
_V
32snss 3750 . . 3  |-  ( A  e.  C  <->  { A }  C_  C )
4 prss.2 . . . 4  |-  B  e. 
_V
54snss 3750 . . 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 3649 . . 3  |-  { A ,  B }  =  ( { A }  u.  { B } )
87sseq1i 3204 . 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 1686   _Vcvv 2790    u. cun 3152    C_ wss 3154   {csn 3642   {cpr 3643
This theorem is referenced by:  tpss  3781  prsspw  3787  uniintsn  3901  pwssun  4301  xpsspwOLD  4800  dffv2  5594  fiint  7135  wunex2  8362  hashfun  11391  prdsle  13363  prdsless  13364  prdsleval  13378  pwsle  13393  acsfn2  13567  clatl  14222  ipoval  14259  ipolerval  14261  eqgfval  14667  eqgval  14668  gaorb  14763  efgcpbllema  15065  frgpuplem  15083  drngnidl  15983  drnglpir  16007  ltbval  16215  ltbwe  16216  opsrle  16219  opsrtoslem1  16227  thlle  16599  isphtpc  18494  shincli  21943  chincli  22041  altxpsspw  24513  axlowdimlem4  24575  toplat  25301  pgapspf2  26064  frgra2v  28188  frgra3vlem1  28189  frgra3vlem2  28190
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-un 3159  df-in 3161  df-ss 3168  df-sn 3648  df-pr 3649
  Copyright terms: Public domain W3C validator