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

Theorem preq1 3959
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 3892 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
21uneq1d 3514 . 2  |-  ( A  =  B  ->  ( { A }  u.  { C } )  =  ( { B }  u.  { C } ) )
3 df-pr 3885 . 2  |-  { A ,  C }  =  ( { A }  u.  { C } )
4 df-pr 3885 . 2  |-  { B ,  C }  =  ( { B }  u.  { C } )
52, 3, 43eqtr4g 2500 1  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    u. cun 3331   {csn 3882   {cpr 3884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-un 3338  df-sn 3883  df-pr 3885
This theorem is referenced by:  preq2  3960  preq12  3961  preq1i  3962  preq1d  3965  tpeq1  3968  prnzg  4000  preq12b  4053  preq12bg  4056  prel12g  4057  opeq1  4064  uniprg  4110  intprg  4167  prex  4539  fprg  5896  opthreg  7829  brdom7disj  8703  brdom6disj  8704  wunpr  8881  wunex2  8910  wuncval2  8919  grupr  8969  joindef  15179  meetdef  15193  pptbas  18617  usgraedg4  23310  usgraidx2vlem2  23315  usgraidx2v  23316  nbgraop  23340  nb3graprlem2  23365  cusgrarn  23372  cusgra2v  23375  nbcusgra  23376  cusgra3v  23377  cusgrafilem2  23393  usgrasscusgra  23396  uvtxnbgra  23406  usgrcyclnl2  23532  4cycl4dv  23558  altopthsn  27997  wwlktovf  30256  usgra2wlkspthlem1  30301  usg2spthonot0  30413  rusgraprop4  30561  rusgrasn  30562  rusgranumwlkl1lem1  30563  rusgranumwlks  30579  frgra2v  30596  frgra3vlem1  30597  frgra3vlem2  30598  3vfriswmgra  30602  3cyclfrgrarn1  30609  4cycl2vnunb  30614  vdn0frgrav2  30621  vdgn0frgrav2  30622  vdn1frgrav2  30623  vdgn1frgrav2  30624  frgrancvvdeqlemB  30636  frgrancvvdeqlemC  30637  frgrawopreglem5  30646  frgrawopreg1  30648  frgraregorufr0  30650  frg2woteqm  30657  usg2spot2nb  30663  extwwlkfablem1  30672  hdmap11lem2  35495
  Copyright terms: Public domain W3C validator