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

Theorem preq1 3875
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 3817 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
21uneq1d 3492 . 2  |-  ( A  =  B  ->  ( { A }  u.  { C } )  =  ( { B }  u.  { C } ) )
3 df-pr 3813 . 2  |-  { A ,  C }  =  ( { A }  u.  { C } )
4 df-pr 3813 . 2  |-  { B ,  C }  =  ( { B }  u.  { C } )
52, 3, 43eqtr4g 2492 1  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    u. cun 3310   {csn 3806   {cpr 3807
This theorem is referenced by:  preq2  3876  preq12  3877  preq1i  3878  preq1d  3881  tpeq1  3884  prnzg  3916  preq12b  3966  preq12bg  3969  opeq1  3976  uniprg  4022  intprg  4076  prex  4398  fprg  5907  opthreg  7565  brdom7disj  8401  brdom6disj  8402  wunpr  8576  wunex2  8605  wuncval2  8614  grupr  8664  joinval  14437  meetval  14444  laspwcl  14658  lanfwcl  14659  pptbas  17064  usgraedg4  21398  usgraidx2vlem2  21403  usgraidx2v  21404  nbgraop  21428  nb3graprlem2  21453  cusgrarn  21460  cusgra2v  21463  nbcusgra  21464  cusgra3v  21465  cusgrafilem2  21481  usgrasscusgra  21484  uvtxnbgra  21494  usgrcyclnl2  21620  4cycl4dv  21646  altopthsn  25798  usgra2wlkspthlem1  28249  usg2spthonot0  28299  frgra2v  28316  frgra3vlem1  28317  frgra3vlem2  28318  3vfriswmgra  28322  3cyclfrgrarn1  28329  4cycl2vnunb  28334  vdn0frgrav2  28341  vdgn0frgrav2  28342  vdn1frgrav2  28343  vdgn1frgrav2  28344  frgrancvvdeqlemB  28354  frgrancvvdeqlemC  28355  frgrawopreglem5  28364  frgrawopreg1  28366  frgraregorufr0  28368  frg2woteqm  28375  usg2spot2nb  28381  hdmap11lem2  32570
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-un 3317  df-sn 3812  df-pr 3813
  Copyright terms: Public domain W3C validator