Theorem elequ2 1823

Description: An identity law for the non-logical predicate. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
elequ2

Proof of Theorem elequ2

Step	Hyp	Ref	Expression
1		ax-9 1822	. 2
2		ax-9 1822	. . 3
3	2	equcoms 1795	. 2
4	1, 3	impbid 191	1

Syntax hints:  ->wi 4  <->wb 184

This theorem is referenced by:  ax12wdemo  1831  dveel2  2112  elsb4  2179  dveel2ALT  2269  ax12el  2272  axext3  2437  axext3OLD  2438  axext4  2439  bm1.1  2440  bm1.1OLD  2441  axrep1  4564  axrep2  4565  axrep3  4566  axrep4  4567  bm1.3ii  4576  nalset  4589  fv3  5884  zfun  6593  tz7.48lem  7125  aceq0  8520  dfac2a  8531  axdc3lem2  8852  zfac  8861  nd2  8984  nd3  8985  axrepndlem2  8989  axunndlem1  8991  axunnd  8992  axpowndlem2  8994  axpowndlem2OLD  8995  axpowndlem3  8996  axpowndlem3OLD  8997  axpowndlem4  8998  axpownd  8999  axregndlem2  9001  axregnd  9002  axregndOLD  9003  axinfndlem1  9004  axacndlem5  9010  zfcndrep  9013  zfcndun  9014  zfcndac  9018  axgroth4  9231  nqereu  9328  rpnnen  13960  mdetunilem9  19122  neiptopnei  19633  2ndc1stc  19952  kqt0lem  20237  regr1lem2  20241  nrmr0reg  20250  hauspwpwf1  20488  dya2iocuni  28254  erdsze  28646  untsucf  29082  untangtr  29086  dfon2lem3  29217  dfon2lem6  29220  dfon2lem7  29221  dfon2lem8  29222  dfon2  29224  axext4dist  29233  distel  29236  axextndbi  29237  fness  30167  fneref  30168  prtlem13  30609  prtlem15  30616  prtlem17  30617  aomclem8  31007  axc11next  31313  bj-elequ2g  34237  bj-elequ12  34239  bj-axext3  34354  bj-axrep1  34374  bj-axrep2  34375  bj-axrep3  34376  bj-axrep4  34377  bj-nalset  34380  bj-eleq2w  34423  bj-axsep2  34493  elintima  37765

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-9 1822

This theorem depends on definitions:  df-bi 185  df-ex 1613