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

Theorem equequ1 1798
 Description: An equivalence law for equality. (Contributed by NM, 1-Aug-1993.) (Proof shortened by Wolf Lammen, 10-Dec-2017.)
Assertion
Ref Expression
equequ1

Proof of Theorem equequ1
StepHypRef Expression
1 ax-7 1790 . 2
2 equtr 1796 . 2
31, 2impbid 191 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184 This theorem is referenced by:  equequ2  1799  drsb1  2118  equsb3lem  2175  dveeq1-o  2265  dveeq1-o16  2266  axc11n-16  2268  ax12eq  2271  sb8eu  2318  2eu6OLD  2384  euequ1OLD  2387  axext3OLD  2438  reu6  3288  reu7  3294  disjxun  4450  cbviota  5561  dff13f  6167  poxp  6912  unxpdomlem1  7744  unxpdomlem2  7745  aceq0  8520  zfac  8861  axrepndlem1  8988  axpowndlem2OLD  8995  zfcndac  9018  injresinj  11926  fsum2dlem  13585  ramub1lem2  14545  ramcl  14547  symgextf1  16446  mamulid  18943  mamurid  18944  mdetdiagid  19102  mdetunilem9  19122  alexsubALTlem3  20549  ptcmplem2  20553  dscmet  21093  dyadmbllem  22008  opnmbllem  22010  isppw2  23389  frg2wot1  25057  disji2f  27438  disjif2  27442  ghomf1olem  29034  wl-equsb3  30004  mblfinlem1  30051  bfp  30320  fphpd  30750  lcoss  33037  ax6e2nd  33331  ax6e2ndVD  33708  ax6e2ndALT  33730  bj-axext3  34354 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 This theorem depends on definitions:  df-bi 185  df-ex 1613
 Copyright terms: Public domain W3C validator