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

Theorem elequ2 2153
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 2152 . 2 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
2 ax9 2152 . . 3 (𝑦 = 𝑥 → (𝑧𝑦𝑧𝑥))
32equcoms 2102 . 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 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854
This theorem is referenced by:  ax12wdemo  2161  dveel2  2508  elsb4  2572  axext3  2742  axext3ALT  2743  axext4  2744  bm1.1  2745  eleq2w  2823  axrep1  4924  axrep2  4925  axrep3  4926  axrep4  4927  axsep2  4934  bm1.3ii  4936  nalset  4947  fv3  6368  zfun  7116  tz7.48lem  7706  aceq1  9150  aceq0  9151  aceq2  9152  dfac2a  9162  kmlem4  9187  axdc3lem2  9485  zfac  9494  nd2  9622  nd3  9623  axrepndlem2  9627  axunndlem1  9629  axunnd  9630  axpowndlem2  9632  axpowndlem3  9633  axpowndlem4  9634  axpownd  9635  axregndlem2  9637  axregnd  9638  axinfndlem1  9639  axacndlem5  9645  zfcndrep  9648  zfcndun  9649  zfcndac  9653  axgroth4  9866  nqereu  9963  mdetunilem9  20648  neiptopnei  21158  2ndc1stc  21476  restlly  21508  kqt0lem  21761  regr1lem2  21765  nrmr0reg  21774  hauspwpwf1  22012  dya2iocuni  30675  erdsze  31512  untsucf  31915  untangtr  31919  dfon2lem3  32016  dfon2lem6  32019  dfon2lem7  32020  dfon2lem8  32021  dfon2  32023  axext4dist  32032  distel  32035  axextndbi  32036  fness  32671  fneref  32672  bj-elequ2g  32994  bj-elequ12  32996  bj-axext3  33097  bj-axrep1  33116  bj-axrep2  33117  bj-axrep3  33118  bj-axrep4  33119  bj-nalset  33122  bj-axc14nf  33165  bj-axsep2  33245  matunitlindflem1  33736  prtlem13  34675  prtlem15  34682  prtlem17  34683  dveel2ALT  34746  ax12el  34749  aomclem8  38151  elintima  38465  axc11next  39127
  Copyright terms: Public domain W3C validator