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

Theorem preq1 4109
Description: Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.)
Assertion
Ref Expression
preq1

Proof of Theorem preq1
StepHypRef Expression
1 sneq 4039 . . 3
21uneq1d 3656 . 2
3 df-pr 4032 . 2
4 df-pr 4032 . 2
52, 3, 43eqtr4g 2523 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  u.cun 3473  {csn 4029  {cpr 4031
This theorem is referenced by:  preq2  4110  preq12  4111  preq1i  4112  preq1d  4115  tpeq1  4118  prnzg  4150  preq12b  4206  preq12bg  4209  prel12g  4210  opeq1  4217  uniprg  4263  intprg  4321  prex  4694  fprg  6080  opthreg  8056  brdom7disj  8930  brdom6disj  8931  wunpr  9108  wunex2  9137  wuncval2  9146  grupr  9196  wwlktovf  12894  joindef  15634  meetdef  15648  pptbas  19509  usgraedg4  24387  usgraidx2vlem2  24392  usgraidx2v  24393  nbgraop  24423  nb3graprlem2  24452  cusgrarn  24459  cusgra2v  24462  nbcusgra  24463  cusgra3v  24464  cusgrafilem2  24480  usgrasscusgra  24483  uvtxnbgra  24493  usgra2wlkspthlem1  24619  usgrcyclnl2  24641  4cycl4dv  24667  usg2spthonot0  24889  rusgraprop4  24944  rusgrasn  24945  rusgranumwwlkl1  24946  rusgranumwlks  24956  frgra2v  24999  frgra3vlem1  25000  frgra3vlem2  25001  3vfriswmgra  25005  3cyclfrgrarn1  25012  4cycl2vnunb  25017  vdn0frgrav2  25023  vdgn0frgrav2  25024  vdn1frgrav2  25025  vdgn1frgrav2  25026  frgrancvvdeqlemB  25038  frgrancvvdeqlemC  25039  frgrawopreglem5  25048  frgrawopreg1  25050  frgraregorufr0  25052  frg2woteqm  25059  usg2spot2nb  25065  extwwlkfablem1  25074  altopthsn  29611  usgvincvad  32404  usgvincvadALT  32407  usgedgvadf1lem2  32414  usgedgvadf1  32415  usgedgvadf1ALTlem2  32417  usgedgvadf1ALT  32418  hdmap11lem2  37572
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-sn 4030  df-pr 4032
  Copyright terms: Public domain W3C validator