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

Theorem preq2 3886
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 3885 . 2  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
2 prcom 3884 . 2  |-  { C ,  A }  =  { A ,  C }
3 prcom 3884 . 2  |-  { C ,  B }  =  { B ,  C }
41, 2, 33eqtr4g 2495 1  |-  ( A  =  B  ->  { C ,  A }  =  { C ,  B }
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653   {cpr 3817
This theorem is referenced by:  preq12  3887  preq2i  3889  preq2d  3892  tpeq2  3895  preq12bg  3979  opeq2  3987  uniprg  4032  intprg  4086  prex  4408  opth  4437  opeqsn  4454  relop  5025  funopg  5487  f1oprswap  5719  fprg  5917  pr2ne  7891  prdom2  7892  dfac2  8013  brdom7disj  8411  brdom6disj  8412  wunpr  8586  wunex2  8615  wuncval2  8624  grupr  8674  prunioo  11027  hashprg  11668  isprm2lem  13088  joinval  14447  meetval  14454  laspwcl  14668  lanfwcl  14669  lspfixed  16202  hmphindis  17831  umgraex  21360  usgraedg4  21408  usgraedgreu  21409  nbgrael  21440  nbgraeledg  21444  nbgranself  21448  nbgraf1olem4  21456  nb3graprlem1  21462  nb3graprlem2  21463  cusgrarn  21470  cusgra1v  21472  cusgra2v  21473  nbcusgra  21474  cusgra3v  21475  usgrasscusgra  21494  uvtxel  21500  uvtxnbgra  21504  cusgrauvtxb  21507  constr2pth  21603  3v3e3cycl1  21633  constr3pthlem3  21646  4cycl4v4e  21655  4cycl4dv  21656  4cycl4dv4e  21657  esumpr2  24460  altopthsn  25808  usgra2pthspth  28307  usgra2wlkspthlem1  28308  usg2spthonot0  28358  frgraunss  28387  frgra1v  28390  frgra2v  28391  frgra3v  28394  1vwmgra  28395  3vfriswmgralem  28396  3vfriswmgra  28397  1to2vfriswmgra  28398  3cyclfrgrarn1  28404  4cycl2vnunb  28409  n4cyclfrgra  28410  vdn0frgrav2  28416  vdgn0frgrav2  28417  vdn1frgrav2  28418  vdgn1frgrav2  28419  frgrancvvdeqlem4  28424  frgrancvvdeqlemB  28429  frgrawopreglem5  28439  frgrawopreg2  28442  frg2woteqm  28450  usg2spot2nb  28456  dihprrn  32226  dvh3dim  32246  mapdindp2  32521
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-un 3327  df-sn 3822  df-pr 3823
  Copyright terms: Public domain W3C validator