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

Theorem prss 4015
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 3518 . 2  |-  ( ( { A }  C_  C  /\  { B }  C_  C )  <->  ( { A }  u.  { B } )  C_  C
)
2 prss.1 . . . 4  |-  A  e. 
_V
32snss 3987 . . 3  |-  ( A  e.  C  <->  { A }  C_  C )
4 prss.2 . . . 4  |-  B  e. 
_V
54snss 3987 . . 3  |-  ( B  e.  C  <->  { B }  C_  C )
63, 5anbi12i 690 . 2  |-  ( ( A  e.  C  /\  B  e.  C )  <->  ( { A }  C_  C  /\  { B }  C_  C ) )
7 df-pr 3868 . . 3  |-  { A ,  B }  =  ( { A }  u.  { B } )
87sseq1i 3368 . 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 1755   _Vcvv 2962    u. cun 3314    C_ wss 3316   {csn 3865   {cpr 3867
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-un 3321  df-in 3323  df-ss 3330  df-sn 3866  df-pr 3868
This theorem is referenced by:  tpss  4026  prsspw  4033  uniintsn  4153  pwssun  4614  xpsspwOLD  4941  dffv2  5752  fiint  7576  wunex2  8893  hashfun  12183  prdsle  14383  prdsless  14384  prdsleval  14398  pwsle  14413  acsfn2  14584  joinfval  15154  joindmss  15160  meetfval  15168  meetdmss  15174  clatl  15269  ipoval  15307  ipolerval  15309  eqgfval  15709  eqgval  15710  gaorb  15805  pmtrrn2  15946  efgcpbllema  16231  frgpuplem  16249  drngnidl  17233  drnglpir  17257  ltbval  17485  ltbwe  17486  opsrle  17489  opsrtoslem1  17497  thlle  17964  isphtpc  20408  axlowdimlem4  23014  usgrarnedg  23126  cusgrarn  23190  shincli  24588  chincli  24686  coinfliprv  26713  altxpsspw  27855  frgraun  30434  frisusgranb  30435  frgra2v  30437  frgra3vlem1  30438  frgra3vlem2  30439  2pthfrgrarn  30447  frgrancvvdeqlem3  30471  isnzr2hash  30605
  Copyright terms: Public domain W3C validator