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

Theorem preq1 3719
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 3664 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
21uneq1d 3341 . 2  |-  ( A  =  B  ->  ( { A }  u.  { C } )  =  ( { B }  u.  { C } ) )
3 df-pr 3660 . 2  |-  { A ,  C }  =  ( { A }  u.  { C } )
4 df-pr 3660 . 2  |-  { B ,  C }  =  ( { B }  u.  { C } )
52, 3, 43eqtr4g 2353 1  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    u. cun 3163   {csn 3653   {cpr 3654
This theorem is referenced by:  preq2  3720  preq12  3721  preq1i  3722  preq1d  3725  tpeq1  3728  prnzg  3759  preq12b  3804  preq12bg  3807  opeq1  3812  uniprg  3858  intprg  3912  prex  4233  opthreg  7335  brdom7disj  8172  brdom6disj  8173  wunpr  8347  wunex2  8376  wuncval2  8385  grupr  8435  joinval  14138  meetval  14145  laspwcl  14359  lanfwcl  14360  pptbas  16761  altopthsn  24567  fprg  25236  nbgraop  28274  nb3graprlem2  28288  cusgra2v  28297  nbcusgra  28298  cusgra3v  28299  uvtxnbgra  28306  cusgrauvtx  28309  usgrcyclnl2  28387  4cycl4dv  28413  frgra2v  28423  frgra3vlem1  28424  frgra3vlem2  28425  3vfriswmgra  28429  3cyclfrgrarn1  28435  4cycl2vnunb  28439  hdmap11lem2  32657
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-sn 3659  df-pr 3660
  Copyright terms: Public domain W3C validator