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

Theorem preq1 4094
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 4024 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
21uneq1d 3642 . 2  |-  ( A  =  B  ->  ( { A }  u.  { C } )  =  ( { B }  u.  { C } ) )
3 df-pr 4017 . 2  |-  { A ,  C }  =  ( { A }  u.  { C } )
4 df-pr 4017 . 2  |-  { B ,  C }  =  ( { B }  u.  { C } )
52, 3, 43eqtr4g 2509 1  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    u. cun 3459   {csn 4014   {cpr 4016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466  df-sn 4015  df-pr 4017
This theorem is referenced by:  preq2  4095  preq12  4096  preq1i  4097  preq1d  4100  tpeq1  4103  prnzg  4135  preq12b  4191  preq12bg  4194  prel12g  4195  opeq1  4202  uniprg  4248  intprg  4306  prex  4679  fprg  6065  opthreg  8038  brdom7disj  8912  brdom6disj  8913  wunpr  9090  wunex2  9119  wuncval2  9128  grupr  9178  wwlktovf  12876  joindef  15613  meetdef  15627  pptbas  19487  usgraedg4  24365  usgraidx2vlem2  24370  usgraidx2v  24371  nbgraop  24401  nb3graprlem2  24430  cusgrarn  24437  cusgra2v  24440  nbcusgra  24441  cusgra3v  24442  cusgrafilem2  24458  usgrasscusgra  24461  uvtxnbgra  24471  usgra2wlkspthlem1  24597  usgrcyclnl2  24619  4cycl4dv  24645  usg2spthonot0  24867  rusgraprop4  24922  rusgrasn  24923  rusgranumwwlkl1  24924  rusgranumwlks  24934  frgra2v  24977  frgra3vlem1  24978  frgra3vlem2  24979  3vfriswmgra  24983  3cyclfrgrarn1  24990  4cycl2vnunb  24995  vdn0frgrav2  25001  vdgn0frgrav2  25002  vdn1frgrav2  25003  vdgn1frgrav2  25004  frgrancvvdeqlemB  25016  frgrancvvdeqlemC  25017  frgrawopreglem5  25026  frgrawopreg1  25028  frgraregorufr0  25030  frg2woteqm  25037  usg2spot2nb  25043  extwwlkfablem1  25052  altopthsn  29587  usgvincvad  32358  usgvincvadALT  32361  usgedgvadf1lem2  32368  usgedgvadf1  32369  usgedgvadf1ALTlem2  32371  usgedgvadf1ALT  32372  hdmap11lem2  37447
  Copyright terms: Public domain W3C validator