MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prss Structured 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 3641 . 2  |-  ( ( { A }  C_  C  /\  { B }  C_  C )  <->  ( { A }  u.  { B } )  C_  C
)
2 prss.1 . . . 4  |-  A  e. 
_V
32snss 4110 . . 3  |-  ( A  e.  C  <->  { A }  C_  C )
4 prss.2 . . . 4  |-  B  e. 
_V
54snss 4110 . . 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 3991 . . 3  |-  { A ,  B }  =  ( { A }  u.  { B } )
87sseq1i 3491 . 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 1758   _Vcvv 3078    u. cun 3437    C_ wss 3439   {csn 3988   {cpr 3990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-un 3444  df-in 3446  df-ss 3453  df-sn 3989  df-pr 3991
This theorem is referenced by:  tpss  4149  prsspw  4156  uniintsn  4276  pwssun  4738  xpsspwOLD  5065  dffv2  5876  fiint  7702  wunex2  9020  hashfun  12321  prdsle  14523  prdsless  14524  prdsleval  14538  pwsle  14553  acsfn2  14724  joinfval  15294  joindmss  15300  meetfval  15308  meetdmss  15314  clatl  15409  ipoval  15447  ipolerval  15449  eqgfval  15852  eqgval  15853  gaorb  15948  pmtrrn2  16089  efgcpbllema  16376  frgpuplem  16394  drngnidl  17444  drnglpir  17468  ltbval  17687  ltbwe  17688  opsrle  17691  opsrtoslem1  17699  thlle  18257  isphtpc  20708  axlowdimlem4  23370  usgrarnedg  23482  cusgrarn  23546  shincli  24944  chincli  25042  coinfliprv  27032  altxpsspw  28175  frgraun  30759  frisusgranb  30760  frgra2v  30762  frgra3vlem1  30763  frgra3vlem2  30764  2pthfrgrarn  30772  frgrancvvdeqlem3  30796  isnzr2hash  30945
  Copyright terms: Public domain W3C validator