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

Theorem prss 3976
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 3507 . 2  |-  ( ( { A }  C_  C  /\  { B }  C_  C )  <->  ( { A }  u.  { B } )  C_  C
)
2 prss.1 . . . 4  |-  A  e. 
_V
32snss 3950 . . 3  |-  ( A  e.  C  <->  { A }  C_  C )
4 prss.2 . . . 4  |-  B  e. 
_V
54snss 3950 . . 3  |-  ( B  e.  C  <->  { B }  C_  C )
63, 5anbi12i 680 . 2  |-  ( ( A  e.  C  /\  B  e.  C )  <->  ( { A }  C_  C  /\  { B }  C_  C ) )
7 df-pr 3845 . . 3  |-  { A ,  B }  =  ( { A }  u.  { B } )
87sseq1i 3358 . 2  |-  ( { A ,  B }  C_  C  <->  ( { A }  u.  { B } )  C_  C
)
91, 6, 83bitr4i 270 1  |-  ( ( A  e.  C  /\  B  e.  C )  <->  { A ,  B }  C_  C )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360    e. wcel 1727   _Vcvv 2962    u. cun 3304    C_ wss 3306   {csn 3838   {cpr 3839
This theorem is referenced by:  tpss  3988  prsspw  3995  uniintsn  4111  pwssun  4518  xpsspwOLD  5016  dffv2  5825  fiint  7412  wunex2  8644  hashfun  11731  prdsle  13715  prdsless  13716  prdsleval  13730  pwsle  13745  acsfn2  13919  clatl  14574  ipoval  14611  ipolerval  14613  eqgfval  15019  eqgval  15020  gaorb  15115  efgcpbllema  15417  frgpuplem  15435  drngnidl  16331  drnglpir  16355  ltbval  16563  ltbwe  16564  opsrle  16567  opsrtoslem1  16575  thlle  16955  isphtpc  19050  usgrarnedg  21435  cusgrarn  21499  shincli  22895  chincli  22993  coinfliprv  24771  altxpsspw  25853  axlowdimlem4  25915  frgraun  28484  frisusgranb  28485  frgra2v  28487  frgra3vlem1  28488  frgra3vlem2  28489  2pthfrgrarn  28497  frgrancvvdeqlem3  28519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-v 2964  df-un 3311  df-in 3313  df-ss 3320  df-sn 3844  df-pr 3845
  Copyright terms: Public domain W3C validator