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

Theorem preq2 3707
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 3706 . 2  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
2 prcom 3705 . 2  |-  { C ,  A }  =  { A ,  C }
3 prcom 3705 . 2  |-  { C ,  B }  =  { B ,  C }
41, 2, 33eqtr4g 2340 1  |-  ( A  =  B  ->  { C ,  A }  =  { C ,  B }
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623   {cpr 3641
This theorem is referenced by:  preq12  3708  preq2i  3710  preq2d  3713  tpeq2  3716  preq12bg  3791  opeq2  3797  uniprg  3842  intprg  3896  prex  4217  opth  4245  opeqsn  4262  relop  4834  funopg  5286  f1oprswap  5515  pr2ne  7635  prdom2  7636  dfac2  7757  brdom7disj  8156  brdom6disj  8157  wunpr  8331  wunex2  8360  wuncval2  8369  grupr  8419  prunioo  10764  hashprg  11368  isprm2lem  12765  joinval  14122  meetval  14129  laspwcl  14343  lanfwcl  14344  lspfixed  15881  hmphindis  17488  esumpr2  23439  umgraex  23875  altopthsn  24495  fprg  25133  nbgrael  28141  nbgraeledg  28145  nbgranself  28149  cusgra1v  28157  cusgra2v  28158  nbcusgra  28159  uvtxel  28161  uvtxisvtx  28162  uvtxnbgra  28165  cusgrauvtx  28168  frgra1v  28176  frgra2v  28177  frgra3v  28180  1vwmgra  28181  3vfriswmgralem  28182  3vfriswmgra  28183  1to2vfriswmgra  28184  dihprrn  31616  dvh3dim  31636  mapdindp2  31911
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-sn 3646  df-pr 3647
  Copyright terms: Public domain W3C validator