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

Theorem preq1 3706
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 3651 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
21uneq1d 3328 . 2  |-  ( A  =  B  ->  ( { A }  u.  { C } )  =  ( { B }  u.  { C } ) )
3 df-pr 3647 . 2  |-  { A ,  C }  =  ( { A }  u.  { C } )
4 df-pr 3647 . 2  |-  { B ,  C }  =  ( { B }  u.  { C } )
52, 3, 43eqtr4g 2340 1  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    u. cun 3150   {csn 3640   {cpr 3641
This theorem is referenced by:  preq2  3707  preq12  3708  preq1i  3709  preq1d  3712  tpeq1  3715  prnzg  3746  preq12b  3788  preq12bg  3791  opeq1  3796  uniprg  3842  intprg  3896  prex  4217  opthreg  7319  brdom7disj  8156  brdom6disj  8157  wunpr  8331  wunex2  8360  wuncval2  8369  grupr  8419  joinval  14122  meetval  14129  laspwcl  14343  lanfwcl  14344  pptbas  16745  altopthsn  24495  fprg  25133  nbgraop  28140  cusgra2v  28158  nbcusgra  28159  uvtxnbgra  28165  cusgrauvtx  28168  frgra2v  28177  frgra3vlem1  28178  frgra3vlem2  28179  3vfriswmgra  28183  hdmap11lem2  32035
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-sn 3646  df-pr 3647
  Copyright terms: Public domain W3C validator