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

Theorem preq1 3827
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 3769 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
21uneq1d 3444 . 2  |-  ( A  =  B  ->  ( { A }  u.  { C } )  =  ( { B }  u.  { C } ) )
3 df-pr 3765 . 2  |-  { A ,  C }  =  ( { A }  u.  { C } )
4 df-pr 3765 . 2  |-  { B ,  C }  =  ( { B }  u.  { C } )
52, 3, 43eqtr4g 2445 1  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    u. cun 3262   {csn 3758   {cpr 3759
This theorem is referenced by:  preq2  3828  preq12  3829  preq1i  3830  preq1d  3833  tpeq1  3836  prnzg  3868  preq12b  3917  preq12bg  3920  opeq1  3927  uniprg  3973  intprg  4027  prex  4348  fprg  5855  opthreg  7507  brdom7disj  8343  brdom6disj  8344  wunpr  8518  wunex2  8547  wuncval2  8556  grupr  8606  joinval  14373  meetval  14380  laspwcl  14594  lanfwcl  14595  pptbas  16996  usgraedg4  21273  usgraidx2vlem2  21278  usgraidx2v  21279  nbgraop  21303  nb3graprlem2  21328  cusgrarn  21335  cusgra2v  21338  nbcusgra  21339  cusgra3v  21340  cusgrafilem2  21356  usgrasscusgra  21359  uvtxnbgra  21369  usgrcyclnl2  21477  4cycl4dv  21503  altopthsn  25521  frgra2v  27753  frgra3vlem1  27754  frgra3vlem2  27755  3vfriswmgra  27759  3cyclfrgrarn1  27766  4cycl2vnunb  27771  vdn0frgrav2  27778  vdgn0frgrav2  27779  vdn1frgrav2  27780  vdgn1frgrav2  27781  frgrancvvdeqlemB  27791  frgrancvvdeqlemC  27792  frgrawopreglem5  27801  frgrawopreg1  27803  frgraregorufr0  27805  hdmap11lem2  31961
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902  df-un 3269  df-sn 3764  df-pr 3765
  Copyright terms: Public domain W3C validator