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

Theorem preq1 3875
Description: Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.)
Assertion
Ref Expression
preq1  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)

Proof of Theorem preq1
StepHypRef Expression
1 sneq 3817 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
21uneq1d 3492 . 2  |-  ( A  =  B  ->  ( { A }  u.  { C } )  =  ( { B }  u.  { C } ) )
3 df-pr 3813 . 2  |-  { A ,  C }  =  ( { A }  u.  { C } )
4 df-pr 3813 . 2  |-  { B ,  C }  =  ( { B }  u.  { C } )
52, 3, 43eqtr4g 2492 1  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    u. cun 3310   {csn 3806   {cpr 3807
This theorem is referenced by:  preq2  3876  preq12  3877  preq1i  3878  preq1d  3881  tpeq1  3884  prnzg  3916  preq12b  3966  preq12bg  3969  opeq1  3976  uniprg  4022  intprg  4076  prex  4398  fprg  5907  opthreg  7565  brdom7disj  8401  brdom6disj  8402  wunpr  8576  wunex2  8605  wuncval2  8614  grupr  8664  joinval  14437  meetval  14444  laspwcl  14658  lanfwcl  14659  pptbas  17064  usgraedg4  21398  usgraidx2vlem2  21403  usgraidx2v  21404  nbgraop  21428  nb3graprlem2  21453  cusgrarn  21460  cusgra2v  21463  nbcusgra  21464  cusgra3v  21465  cusgrafilem2  21481  usgrasscusgra  21484  uvtxnbgra  21494  usgrcyclnl2  21620  4cycl4dv  21646  altopthsn  25798  usgra2wlkspthlem1  28259  usg2spthonot0  28309  frgra2v  28326  frgra3vlem1  28327  frgra3vlem2  28328  3vfriswmgra  28332  3cyclfrgrarn1  28339  4cycl2vnunb  28344  vdn0frgrav2  28351  vdgn0frgrav2  28352  vdn1frgrav2  28353  vdgn1frgrav2  28354  frgrancvvdeqlemB  28364  frgrancvvdeqlemC  28365  frgrawopreglem5  28374  frgrawopreg1  28376  frgraregorufr0  28378  frg2woteqm  28385  usg2spot2nb  28391  hdmap11lem2  32580
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-sn 3812  df-pr 3813
  Copyright terms: Public domain W3C validator