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

Theorem elequ2 2001
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 2000 . 2 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
2 ax9 2000 . . 3 (𝑦 = 𝑥 → (𝑧𝑦𝑧𝑥))
32equcoms 1944 . 2 (𝑥 = 𝑦 → (𝑧𝑦𝑧𝑥))
41, 3impbid 202 1 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702
This theorem is referenced by:  ax12wdemo  2009  dveel2  2370  elsb4  2434  axext3  2603  axext3ALT  2604  axext4  2605  bm1.1  2606  axrep1  4742  axrep2  4743  axrep3  4744  axrep4  4745  axsep2  4752  bm1.3ii  4754  nalset  4765  fv3  6173  zfun  6915  tz7.48lem  7496  aceq1  8900  aceq0  8901  aceq2  8902  dfac2a  8912  kmlem4  8935  axdc3lem2  9233  zfac  9242  nd2  9370  nd3  9371  axrepndlem2  9375  axunndlem1  9377  axunnd  9378  axpowndlem2  9380  axpowndlem3  9381  axpowndlem4  9382  axpownd  9383  axregndlem2  9385  axregnd  9386  axinfndlem1  9387  axacndlem5  9393  zfcndrep  9396  zfcndun  9397  zfcndac  9401  axgroth4  9614  nqereu  9711  mdetunilem9  20366  neiptopnei  20876  2ndc1stc  21194  restlly  21226  kqt0lem  21479  regr1lem2  21483  nrmr0reg  21492  hauspwpwf1  21731  dya2iocuni  30168  erdsze  30945  untsucf  31348  untangtr  31352  dfon2lem3  31444  dfon2lem6  31447  dfon2lem7  31448  dfon2lem8  31449  dfon2  31451  axext4dist  31460  distel  31463  axextndbi  31464  fness  32039  fneref  32040  bj-elequ2g  32361  bj-elequ12  32363  bj-axext3  32465  bj-axrep1  32484  bj-axrep2  32485  bj-axrep3  32486  bj-axrep4  32487  bj-nalset  32490  bj-eleq2w  32547  bj-axsep2  32621  matunitlindflem1  33076  prtlem13  33672  prtlem15  33679  prtlem17  33680  dveel2ALT  33743  ax12el  33746  aomclem8  37150  elintima  37465  axc11next  38128
  Copyright terms: Public domain W3C validator