MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elequ2 Structured version   Visualization version   GIF version

Theorem elequ2 1989
Description: An identity law for the non-logical predicate. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
elequ2 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))

Proof of Theorem elequ2
StepHypRef Expression
1 ax9 1988 . 2 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
2 ax9 1988 . . 3 (𝑦 = 𝑥 → (𝑧𝑦𝑧𝑥))
32equcoms 1932 . 2 (𝑥 = 𝑦 → (𝑧𝑦𝑧𝑥))
41, 3impbid 200 1 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-9 1984
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695
This theorem is referenced by:  ax12wdemo  1997  dveel2  2354  elsb4  2418  axext3  2587  axext3ALT  2588  axext4  2589  bm1.1  2590  axrep1  4690  axrep2  4691  axrep3  4692  axrep4  4693  bm1.3ii  4702  nalset  4714  fv3  6097  zfun  6821  tz7.48lem  7396  aceq0  8797  dfac2a  8808  axdc3lem2  9129  zfac  9138  nd2  9262  nd3  9263  axrepndlem2  9267  axunndlem1  9269  axunnd  9270  axpowndlem2  9272  axpowndlem3  9273  axpowndlem4  9274  axpownd  9275  axregndlem2  9277  axregnd  9278  axinfndlem1  9279  axacndlem5  9285  zfcndrep  9288  zfcndun  9289  zfcndac  9293  axgroth4  9506  nqereu  9603  mdetunilem9  20183  neiptopnei  20684  2ndc1stc  21002  kqt0lem  21287  regr1lem2  21291  nrmr0reg  21300  hauspwpwf1  21539  dya2iocuni  29474  erdsze  30240  untsucf  30643  untangtr  30647  dfon2lem3  30736  dfon2lem6  30739  dfon2lem7  30740  dfon2lem8  30741  dfon2  30743  axext4dist  30752  distel  30755  axextndbi  30756  fness  31316  fneref  31317  bj-elequ2g  31655  bj-elequ12  31657  bj-axext3  31766  bj-axrep1  31785  bj-axrep2  31786  bj-axrep3  31787  bj-axrep4  31788  bj-nalset  31791  bj-eleq2w  31840  bj-axsep2  31912  matunitlindflem1  32374  prtlem13  32970  prtlem15  32977  prtlem17  32978  dveel2ALT  33041  ax12el  33044  aomclem8  36448  elintima  36763  axc11next  37428
  Copyright terms: Public domain W3C validator