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

Theorem preq1 3942
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 3875 . . 3  |-  ( A  =  B  ->  { A }  =  { B } )
21uneq1d 3497 . 2  |-  ( A  =  B  ->  ( { A }  u.  { C } )  =  ( { B }  u.  { C } ) )
3 df-pr 3868 . 2  |-  { A ,  C }  =  ( { A }  u.  { C } )
4 df-pr 3868 . 2  |-  { B ,  C }  =  ( { B }  u.  { C } )
52, 3, 43eqtr4g 2490 1  |-  ( A  =  B  ->  { A ,  C }  =  { B ,  C }
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    u. cun 3314   {csn 3865   {cpr 3867
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-un 3321  df-sn 3866  df-pr 3868
This theorem is referenced by:  preq2  3943  preq12  3944  preq1i  3945  preq1d  3948  tpeq1  3951  prnzg  3983  preq12b  4036  preq12bg  4039  prel12g  4040  opeq1  4047  uniprg  4093  intprg  4150  prex  4522  fprg  5878  opthreg  7812  brdom7disj  8686  brdom6disj  8687  wunpr  8863  wunex2  8892  wuncval2  8901  grupr  8951  joindef  15156  meetdef  15170  pptbas  18453  usgraedg4  23127  usgraidx2vlem2  23132  usgraidx2v  23133  nbgraop  23157  nb3graprlem2  23182  cusgrarn  23189  cusgra2v  23192  nbcusgra  23193  cusgra3v  23194  cusgrafilem2  23210  usgrasscusgra  23213  uvtxnbgra  23223  usgrcyclnl2  23349  4cycl4dv  23375  altopthsn  27838  wwlktovf  30094  usgra2wlkspthlem1  30139  usg2spthonot0  30251  rusgraprop4  30399  rusgrasn  30400  rusgranumwlkl1lem1  30401  rusgranumwlks  30417  frgra2v  30434  frgra3vlem1  30435  frgra3vlem2  30436  3vfriswmgra  30440  3cyclfrgrarn1  30447  4cycl2vnunb  30452  vdn0frgrav2  30459  vdgn0frgrav2  30460  vdn1frgrav2  30461  vdgn1frgrav2  30462  frgrancvvdeqlemB  30474  frgrancvvdeqlemC  30475  frgrawopreglem5  30484  frgrawopreg1  30486  frgraregorufr0  30488  frg2woteqm  30495  usg2spot2nb  30501  extwwlkfablem1  30510  hdmap11lem2  35060
  Copyright terms: Public domain W3C validator