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

Theorem prss 4138
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 3619 . 2  |-  ( ( { A }  C_  C  /\  { B }  C_  C )  <->  ( { A }  u.  { B } )  C_  C
)
2 prss.1 . . . 4  |-  A  e. 
_V
32snss 4108 . . 3  |-  ( A  e.  C  <->  { A }  C_  C )
4 prss.2 . . . 4  |-  B  e. 
_V
54snss 4108 . . 3  |-  ( B  e.  C  <->  { B }  C_  C )
63, 5anbi12i 708 . 2  |-  ( ( A  e.  C  /\  B  e.  C )  <->  ( { A }  C_  C  /\  { B }  C_  C ) )
7 df-pr 3982 . . 3  |-  { A ,  B }  =  ( { A }  u.  { B } )
87sseq1i 3467 . 2  |-  ( { A ,  B }  C_  C  <->  ( { A }  u.  { B } )  C_  C
)
91, 6, 83bitr4i 285 1  |-  ( ( A  e.  C  /\  B  e.  C )  <->  { A ,  B }  C_  C )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    /\ wa 375    e. wcel 1897   _Vcvv 3056    u. cun 3413    C_ wss 3415   {csn 3979   {cpr 3981
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-un 3420  df-in 3422  df-ss 3429  df-sn 3980  df-pr 3982
This theorem is referenced by:  tpss  4149  prsspwOLD  4157  uniintsn  4285  pwssun  4758  xpsspw  4966  dffv2  5960  fpr2g  6149  fiint  7873  wunex2  9188  hashfun  12641  prdsle  15408  prdsless  15409  prdsleval  15423  pwsle  15438  acsfn2  15617  joinfval  16295  joindmss  16301  meetfval  16309  meetdmss  16315  clatl  16410  ipoval  16448  ipolerval  16450  eqgfval  16913  eqgval  16914  gaorb  17009  pmtrrn2  17149  efgcpbllema  17452  frgpuplem  17470  drngnidl  18501  drnglpir  18525  isnzr2hash  18536  ltbval  18743  ltbwe  18744  opsrle  18747  opsrtoslem1  18755  thlle  19308  isphtpc  22073  axlowdimlem4  25023  usgrarnedg  25159  cusgrarn  25235  frgraun  25772  frisusgranb  25773  frgra2v  25775  frgra3vlem1  25776  frgra3vlem2  25777  2pthfrgrarn  25785  frgrancvvdeqlem3  25808  shincli  27063  chincli  27161  coinfliprv  29363  altxpsspw  30792  fourierdlem103  38110  fourierdlem104  38111  nnsum3primes4  38920  fun2dmnop  39068  structgrssvtxlem  39170  structgrssvtx  39171  structgrssiedg  39172  umgredg  39276  1wlk1walk  39696  1wlkdlem2  39725  31wlkdlem6  39905
  Copyright terms: Public domain W3C validator