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

Theorem prss 4165
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 3660 . 2  |-  ( ( { A }  C_  C  /\  { B }  C_  C )  <->  ( { A }  u.  { B } )  C_  C
)
2 prss.1 . . . 4  |-  A  e. 
_V
32snss 4135 . . 3  |-  ( A  e.  C  <->  { A }  C_  C )
4 prss.2 . . . 4  |-  B  e. 
_V
54snss 4135 . . 3  |-  ( B  e.  C  <->  { B }  C_  C )
63, 5anbi12i 697 . 2  |-  ( ( A  e.  C  /\  B  e.  C )  <->  ( { A }  C_  C  /\  { B }  C_  C ) )
7 df-pr 4013 . . 3  |-  { A ,  B }  =  ( { A }  u.  { B } )
87sseq1i 3510 . 2  |-  ( { A ,  B }  C_  C  <->  ( { A }  u.  { B } )  C_  C
)
91, 6, 83bitr4i 277 1  |-  ( ( A  e.  C  /\  B  e.  C )  <->  { A ,  B }  C_  C )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    e. wcel 1802   _Vcvv 3093    u. cun 3456    C_ wss 3458   {csn 4010   {cpr 4012
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-un 3463  df-in 3465  df-ss 3472  df-sn 4011  df-pr 4013
This theorem is referenced by:  tpss  4176  prsspwOLD  4183  uniintsn  4305  pwssun  4772  xpsspwOLD  5103  dffv2  5927  fiint  7795  wunex2  9114  hashfun  12469  prdsle  14731  prdsless  14732  prdsleval  14746  pwsle  14761  acsfn2  14932  joinfval  15500  joindmss  15506  meetfval  15514  meetdmss  15520  clatl  15615  ipoval  15653  ipolerval  15655  eqgfval  16118  eqgval  16119  gaorb  16214  pmtrrn2  16354  efgcpbllema  16641  frgpuplem  16659  drngnidl  17745  drnglpir  17769  isnzr2hash  17780  ltbval  18004  ltbwe  18005  opsrle  18008  opsrtoslem1  18016  thlle  18595  isphtpc  21360  axlowdimlem4  24113  usgrarnedg  24249  cusgrarn  24324  frgraun  24861  frisusgranb  24862  frgra2v  24864  frgra3vlem1  24865  frgra3vlem2  24866  2pthfrgrarn  24874  frgrancvvdeqlem3  24897  shincli  26145  chincli  26243  coinfliprv  28287  altxpsspw  29595  fourierdlem103  31877  fourierdlem104  31878
  Copyright terms: Public domain W3C validator