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

Theorem elequ1 1821
Description: An identity law for the non-logical predicate. (Contributed by NM, 30-Jun-1993.)
Assertion
Ref Expression
elequ1

Proof of Theorem elequ1
StepHypRef Expression
1 ax-8 1820 . 2
2 ax-8 1820 . . 3
32equcoms 1795 . 2
41, 3impbid 191 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  ax12wdemo  1831  cleljust  2109  cleljustALT  2110  dveel1  2111  axc14  2113  elsb3  2178  ax12el  2272  axsep  4572  nalset  4589  zfpow  4631  zfun  6593  tz7.48lem  7125  unxpdomlem1  7744  pssnn  7758  zfinf  8077  aceq0  8520  dfac3  8523  dfac5lem2  8526  dfac5lem3  8527  dfac2a  8531  zfac  8861  nd1  8983  axextnd  8987  axrepndlem1  8988  axrepndlem2  8989  axunndlem1  8991  axunnd  8992  axpowndlem2  8994  axpowndlem2OLD  8995  axpowndlem3  8996  axpowndlem3OLD  8997  axpowndlem4  8998  axregndlem1  9000  axregnd  9002  axregndOLD  9003  zfcndun  9014  zfcndpow  9015  zfcndinf  9017  zfcndac  9018  fpwwe2lem12  9040  axgroth3  9230  axgroth4  9231  nqereu  9328  rpnnen  13960  mdetunilem9  19122  madugsum  19145  neiptopnei  19633  2ndc1stc  19952  nrmr0reg  20250  alexsubALTlem4  20550  xrsmopn  21317  itg2cn  22170  itgcn  22249  sqff1o  23456  dya2iocuni  28254  erdsze  28646  untsucf  29082  untangtr  29086  dfon2lem3  29217  dfon2lem6  29220  dfon2lem7  29221  dfon2  29224  axextdist  29232  distel  29236  neibastop2lem  30178  prtlem5  30597  pw2f1ocnv  30979  aomclem8  31007  lcosslsp  33039  bnj849  33983  bj-elequ12  34239  bj-cleljust  34344  bj-axsep  34379  bj-nalset  34380  bj-zfpow  34381  bj-ru0  34500
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-8 1820
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator