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

Theorem preq1 4106
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 4037 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
21uneq1d 3657 . 2  |-  ( A  =  B  ->  ( { A }  u.  { C } )  =  ( { B }  u.  { C } ) )
3 df-pr 4030 . 2  |-  { A ,  C }  =  ( { A }  u.  { C } )
4 df-pr 4030 . 2  |-  { B ,  C }  =  ( { B }  u.  { C } )
52, 3, 43eqtr4g 2533 1  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    u. cun 3474   {csn 4027   {cpr 4029
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-sn 4028  df-pr 4030
This theorem is referenced by:  preq2  4107  preq12  4108  preq1i  4109  preq1d  4112  tpeq1  4115  prnzg  4147  preq12b  4202  preq12bg  4205  prel12g  4206  opeq1  4213  uniprg  4259  intprg  4316  prex  4689  fprg  6068  opthreg  8031  brdom7disj  8905  brdom6disj  8906  wunpr  9083  wunex2  9112  wuncval2  9121  grupr  9171  wwlktovf  12853  joindef  15487  meetdef  15501  pptbas  19275  usgraedg4  24063  usgraidx2vlem2  24068  usgraidx2v  24069  nbgraop  24099  nb3graprlem2  24128  cusgrarn  24135  cusgra2v  24138  nbcusgra  24139  cusgra3v  24140  cusgrafilem2  24156  usgrasscusgra  24159  uvtxnbgra  24169  usgra2wlkspthlem1  24295  usgrcyclnl2  24317  4cycl4dv  24343  usg2spthonot0  24565  rusgraprop4  24620  rusgrasn  24621  rusgranumwwlkl1  24622  rusgranumwlks  24632  frgra2v  24675  frgra3vlem1  24676  frgra3vlem2  24677  3vfriswmgra  24681  3cyclfrgrarn1  24688  4cycl2vnunb  24693  vdn0frgrav2  24700  vdgn0frgrav2  24701  vdn1frgrav2  24702  vdgn1frgrav2  24703  frgrancvvdeqlemB  24715  frgrancvvdeqlemC  24716  frgrawopreglem5  24725  frgrawopreg1  24727  frgraregorufr0  24729  frg2woteqm  24736  usg2spot2nb  24742  extwwlkfablem1  24751  altopthsn  29188  usgvincvad  31873  usgvincvadALT  31876  usgedgvadf1lem2  31883  usgedgvadf1  31884  usgedgvadf1ALTlem2  31886  usgedgvadf1ALT  31887  hdmap11lem2  36642
  Copyright terms: Public domain W3C validator