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

Theorem preq2 4110
Description: Equality theorem for unordered pairs. (Contributed by NM, 15-Jul-1993.)
Assertion
Ref Expression
preq2

Proof of Theorem preq2
StepHypRef Expression
1 preq1 4109 . 2
2 prcom 4108 . 2
3 prcom 4108 . 2
41, 2, 33eqtr4g 2523 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  {cpr 4031
This theorem is referenced by:  preq12  4111  preq2i  4113  preq2d  4116  tpeq2  4119  preq12bg  4209  prel12g  4210  opeq2  4218  uniprg  4263  intprg  4321  prex  4694  opth  4726  opeqsn  4748  relop  5158  funopg  5625  f1oprswap  5860  fprg  6080  fnprb  6129  pr2ne  8404  prdom2  8405  dfac2  8532  brdom7disj  8930  brdom6disj  8931  wunpr  9108  wunex2  9137  wuncval2  9146  grupr  9196  prunioo  11678  hashprg  12460  wwlktovf  12894  wwlktovfo  12896  wrd2f1tovbij  12898  isprm2lem  14224  joindef  15634  meetdef  15648  lspfixed  17774  hmphindis  20298  umgraex  24323  usgraedg4  24387  usgraedgreu  24388  nbgrael  24426  nbgraeledg  24430  nbgranself  24434  nbgraf1olem4  24444  nb3graprlem1  24451  nb3graprlem2  24452  cusgrarn  24459  cusgra1v  24461  cusgra2v  24462  nbcusgra  24463  cusgra3v  24464  usgrasscusgra  24483  uvtxel  24489  uvtxnbgra  24493  cusgrauvtxb  24496  uvtxnb  24497  constr2pth  24603  usgra2wlkspthlem1  24619  3v3e3cycl1  24644  constr3pthlem3  24657  4cycl4v4e  24666  4cycl4dv  24667  4cycl4dv4e  24668  wwlkextfun  24729  wwlkextsur  24731  wwlkextbij  24733  clwlkisclwwlklem1  24787  usg2spthonot0  24889  frgraunss  24995  frgra1v  24998  frgra2v  24999  frgra3v  25002  1vwmgra  25003  3vfriswmgralem  25004  3vfriswmgra  25005  1to2vfriswmgra  25006  3cyclfrgrarn1  25012  4cycl2vnunb  25017  n4cyclfrgra  25018  vdn0frgrav2  25023  vdgn0frgrav2  25024  vdn1frgrav2  25025  vdgn1frgrav2  25026  frgrancvvdeqlem4  25033  frgrancvvdeqlemB  25038  frgrawopreglem5  25048  frgrawopreg2  25051  frg2woteqm  25059  usg2spot2nb  25065  numclwwlkovf2ex  25086  esumpr2  28074  altopthsn  29611  usgra2pthspth  32351  usgvincvad  32404  usgvincvadeu  32405  usgvincvadALT  32407  usgvincvadeuALT  32408  dihprrn  37153  dvh3dim  37173  mapdindp2  37448
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