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

Theorem prss 3944
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 3513 . 2  |-  ( ( { A }  C_  C  /\  { B }  C_  C )  <->  ( { A }  u.  { B } )  C_  C
)
2 prss.1 . . . 4  |-  A  e. 
_V
32snss 3918 . . 3  |-  ( A  e.  C  <->  { A }  C_  C )
4 prss.2 . . . 4  |-  B  e. 
_V
54snss 3918 . . 3  |-  ( B  e.  C  <->  { B }  C_  C )
63, 5anbi12i 679 . 2  |-  ( ( A  e.  C  /\  B  e.  C )  <->  ( { A }  C_  C  /\  { B }  C_  C ) )
7 df-pr 3813 . . 3  |-  { A ,  B }  =  ( { A }  u.  { B } )
87sseq1i 3364 . 2  |-  ( { A ,  B }  C_  C  <->  ( { A }  u.  { B } )  C_  C
)
91, 6, 83bitr4i 269 1  |-  ( ( A  e.  C  /\  B  e.  C )  <->  { A ,  B }  C_  C )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359    e. wcel 1725   _Vcvv 2948    u. cun 3310    C_ wss 3312   {csn 3806   {cpr 3807
This theorem is referenced by:  tpss  3956  prsspw  3963  uniintsn  4079  pwssun  4481  xpsspwOLD  4978  dffv2  5787  fiint  7374  wunex2  8602  hashfun  11688  prdsle  13672  prdsless  13673  prdsleval  13687  pwsle  13702  acsfn2  13876  clatl  14531  ipoval  14568  ipolerval  14570  eqgfval  14976  eqgval  14977  gaorb  15072  efgcpbllema  15374  frgpuplem  15392  drngnidl  16288  drnglpir  16312  ltbval  16520  ltbwe  16521  opsrle  16524  opsrtoslem1  16532  thlle  16912  isphtpc  19007  usgrarnedg  21392  cusgrarn  21456  shincli  22852  chincli  22950  coinfliprv  24728  altxpsspw  25770  axlowdimlem4  25832  frgraun  28244  frisusgranb  28245  frgra2v  28247  frgra3vlem1  28248  frgra3vlem2  28249  2pthfrgrarn  28257  frgrancvvdeqlem3  28279
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-un 3317  df-in 3319  df-ss 3326  df-sn 3812  df-pr 3813
  Copyright terms: Public domain W3C validator