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

Theorem prss 3770
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 3350 . 2  |-  ( ( { A }  C_  C  /\  { B }  C_  C )  <->  ( { A }  u.  { B } )  C_  C
)
2 prss.1 . . . 4  |-  A  e. 
_V
32snss 3749 . . 3  |-  ( A  e.  C  <->  { A }  C_  C )
4 prss.2 . . . 4  |-  B  e. 
_V
54snss 3749 . . 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 3648 . . 3  |-  { A ,  B }  =  ( { A }  u.  { B } )
87sseq1i 3203 . 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 1685   _Vcvv 2789    u. cun 3151    C_ wss 3153   {csn 3641   {cpr 3642
This theorem is referenced by:  tpss  3780  prsspw  3786  uniintsn  3900  pwssun  4298  xpsspwOLD  4797  dffv2  5554  fiint  7129  wunex2  8356  hashfun  11385  prdsle  13357  prdsless  13358  prdsleval  13372  pwsle  13387  acsfn2  13561  clatl  14216  ipoval  14253  ipolerval  14255  eqgfval  14661  eqgval  14662  gaorb  14757  efgcpbllema  15059  frgpuplem  15077  drngnidl  15977  drnglpir  16001  ltbval  16209  ltbwe  16210  opsrle  16213  opsrtoslem1  16221  thlle  16593  isphtpc  18488  shincli  21937  chincli  22035  altxpsspw  23921  axlowdimlem4  23983  toplat  24701  pgapspf2  25464
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 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
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 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-un 3158  df-in 3160  df-ss 3167  df-sn 3647  df-pr 3648
  Copyright terms: Public domain W3C validator