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

Theorem prss 3743
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 3324 . 2  |-  ( ( { A }  C_  C  /\  { B }  C_  C )  <->  ( { A }  u.  { B } )  C_  C
)
2 prss.1 . . . 4  |-  A  e. 
_V
32snss 3722 . . 3  |-  ( A  e.  C  <->  { A }  C_  C )
4 prss.2 . . . 4  |-  B  e. 
_V
54snss 3722 . . 3  |-  ( B  e.  C  <->  { B }  C_  C )
63, 5anbi12i 681 . 2  |-  ( ( A  e.  C  /\  B  e.  C )  <->  ( { A }  C_  C  /\  { B }  C_  C ) )
7 df-pr 3621 . . 3  |-  { A ,  B }  =  ( { A }  u.  { B } )
87sseq1i 3177 . 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 1621   _Vcvv 2763    u. cun 3125    C_ wss 3127   {csn 3614   {cpr 3615
This theorem is referenced by:  tpss  3753  prsspw  3759  uniintsn  3873  pwssun  4271  xpsspwOLD  4786  dffv2  5526  fiint  7101  wunex2  8328  hashfun  11355  prdsle  13324  prdsless  13325  prdsleval  13339  pwsle  13354  acsfn2  13528  clatl  14183  ipoval  14220  ipolerval  14222  eqgfval  14628  eqgval  14629  gaorb  14724  efgcpbllema  15026  frgpuplem  15044  drngnidl  15944  drnglpir  15968  ltbval  16176  ltbwe  16177  opsrle  16180  opsrtoslem1  16188  thlle  16560  isphtpc  18455  shincli  21902  chincli  22000  altxpsspw  23887  axlowdimlem4  23949  toplat  24658  pgapspf2  25421
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-un 3132  df-in 3134  df-ss 3141  df-sn 3620  df-pr 3621
  Copyright terms: Public domain W3C validator