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

Theorem preq1 3740
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 3685 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
21uneq1d 3362 . 2  |-  ( A  =  B  ->  ( { A }  u.  { C } )  =  ( { B }  u.  { C } ) )
3 df-pr 3681 . 2  |-  { A ,  C }  =  ( { A }  u.  { C } )
4 df-pr 3681 . 2  |-  { B ,  C }  =  ( { B }  u.  { C } )
52, 3, 43eqtr4g 2373 1  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1633    u. cun 3184   {csn 3674   {cpr 3675
This theorem is referenced by:  preq2  3741  preq12  3742  preq1i  3743  preq1d  3746  tpeq1  3749  prnzg  3780  preq12b  3825  preq12bg  3828  opeq1  3833  uniprg  3879  intprg  3933  prex  4254  fprg  5743  opthreg  7364  brdom7disj  8201  brdom6disj  8202  wunpr  8376  wunex2  8405  wuncval2  8414  grupr  8464  joinval  14171  meetval  14178  laspwcl  14392  lanfwcl  14393  pptbas  16801  altopthsn  24881  usgraedg4  27357  nbgraop  27373  nb3graprlem2  27398  cusgra2v  27407  nbcusgra  27408  cusgra3v  27409  uvtxnbgra  27416  cusgrauvtx  27419  usgrcyclnl2  27525  4cycl4dv  27551  frgra2v  27591  frgra3vlem1  27592  frgra3vlem2  27593  3vfriswmgra  27597  3cyclfrgrarn1  27604  4cycl2vnunb  27609  vdn0frgrav2  27616  vdgn0frgrav2  27617  vdn1frgrav2  27618  vdgn1frgrav2  27619  frgrancvvdeqlemB  27630  frgrancvvdeqlemC  27631  hdmap11lem2  31853
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-v 2824  df-un 3191  df-sn 3680  df-pr 3681
  Copyright terms: Public domain W3C validator