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

Theorem preq1 4023
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 3954 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
21uneq1d 3571 . 2  |-  ( A  =  B  ->  ( { A }  u.  { C } )  =  ( { B }  u.  { C } ) )
3 df-pr 3947 . 2  |-  { A ,  C }  =  ( { A }  u.  { C } )
4 df-pr 3947 . 2  |-  { B ,  C }  =  ( { B }  u.  { C } )
52, 3, 43eqtr4g 2448 1  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399    u. cun 3387   {csn 3944   {cpr 3946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-un 3394  df-sn 3945  df-pr 3947
This theorem is referenced by:  preq2  4024  preq12  4025  preq1i  4026  preq1d  4029  tpeq1  4032  prnzg  4064  preq12b  4120  preq12bg  4123  prel12g  4124  opeq1  4131  uniprg  4177  intprg  4234  prex  4604  fprg  5982  opthreg  7949  brdom7disj  8822  brdom6disj  8823  wunpr  8998  wunex2  9027  wuncval2  9036  grupr  9086  wwlktovf  12805  joindef  15751  meetdef  15765  pptbas  19594  usgraedg4  24508  usgraidx2vlem2  24513  usgraidx2v  24514  nbgraop  24544  nb3graprlem2  24573  cusgrarn  24580  cusgra2v  24583  nbcusgra  24584  cusgra3v  24585  cusgrafilem2  24601  usgrasscusgra  24604  uvtxnbgra  24614  usgra2wlkspthlem1  24740  usgrcyclnl2  24762  4cycl4dv  24788  usg2spthonot0  25010  rusgraprop4  25065  rusgrasn  25066  rusgranumwwlkl1  25067  rusgranumwlks  25077  frgra2v  25120  frgra3vlem1  25121  frgra3vlem2  25122  3vfriswmgra  25126  3cyclfrgrarn1  25133  4cycl2vnunb  25138  vdn0frgrav2  25144  vdgn0frgrav2  25145  vdn1frgrav2  25146  vdgn1frgrav2  25147  frgrancvvdeqlemB  25159  frgrancvvdeqlemC  25160  frgrawopreglem5  25169  frgrawopreg1  25171  frgraregorufr0  25173  frg2woteqm  25180  usg2spot2nb  25186  extwwlkfablem1  25195  altopthsn  29764  usgvincvad  32722  usgvincvadALT  32725  usgedgvadf1lem2  32732  usgedgvadf1  32733  usgedgvadf1ALTlem2  32735  usgedgvadf1ALT  32736  hdmap11lem2  37985
  Copyright terms: Public domain W3C validator