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

Theorem preq2 3720
Description: Equality theorem for unordered pairs. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
preq2  |-  ( A  =  B  ->  { C ,  A }  =  { C ,  B }
)

Proof of Theorem preq2
StepHypRef Expression
1 preq1 3719 . 2  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
2 prcom 3718 . 2  |-  { C ,  A }  =  { A ,  C }
3 prcom 3718 . 2  |-  { C ,  B }  =  { B ,  C }
41, 2, 33eqtr4g 2353 1  |-  ( A  =  B  ->  { C ,  A }  =  { C ,  B }
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   {cpr 3654
This theorem is referenced by:  preq12  3721  preq2i  3723  preq2d  3726  tpeq2  3729  preq12bg  3807  opeq2  3813  uniprg  3858  intprg  3912  prex  4233  opth  4261  opeqsn  4278  relop  4850  funopg  5302  f1oprswap  5531  pr2ne  7651  prdom2  7652  dfac2  7773  brdom7disj  8172  brdom6disj  8173  wunpr  8347  wunex2  8376  wuncval2  8385  grupr  8435  prunioo  10780  hashprg  11384  isprm2lem  12781  joinval  14138  meetval  14145  laspwcl  14359  lanfwcl  14360  lspfixed  15897  hmphindis  17504  esumpr2  23454  umgraex  23890  altopthsn  24567  fprg  25236  nbgrael  28275  nbgraeledg  28279  nbgranself  28283  nb3graprlem1  28287  nb3graprlem2  28288  cusgra1v  28296  cusgra2v  28297  nbcusgra  28298  cusgra3v  28299  uvtxel  28302  uvtxisvtx  28303  uvtxnbgra  28306  cusgrauvtx  28309  3v3e3cycl1  28390  constr3pthlem3  28403  4cycl4v4e  28412  4cycl4dv  28413  4cycl4dv4e  28414  frgra1v  28422  frgra2v  28423  frgra3v  28426  1vwmgra  28427  3vfriswmgralem  28428  3vfriswmgra  28429  1to2vfriswmgra  28430  3cyclfrgrarn1  28435  4cycl2vnunb  28439  n4cyclfrgra  28440  dihprrn  32238  dvh3dim  32258  mapdindp2  32533
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-sn 3659  df-pr 3660
  Copyright terms: Public domain W3C validator