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

Theorem elequ1 2150
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 ax8 2149 . 2 (𝑥 = 𝑦 → (𝑥𝑧𝑦𝑧))
2 ax8 2149 . . 3 (𝑦 = 𝑥 → (𝑦𝑧𝑥𝑧))
32equcoms 2103 . 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 1868  ax-4 1883  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2145
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1851
This theorem is referenced by:  cleljust  2151  ax12wdemo  2165  cleljustALT  2345  cleljustALT2  2346  dveel1  2515  axc14  2517  elsb3lem  2580  elsb3OLD  2582  axsep  4910  nalset  4925  zfpow  4971  zfun  7095  tz7.48lem  7687  unxpdomlem1  8318  pssnn  8332  zfinf  8698  aceq0  9139  dfac3  9142  dfac5lem2  9145  dfac5lem3  9146  dfac2a  9150  zfac  9482  nd1  9609  axextnd  9613  axrepndlem1  9614  axrepndlem2  9615  axunndlem1  9617  axunnd  9618  axpowndlem2  9620  axpowndlem3  9621  axpowndlem4  9622  axregndlem1  9624  axregnd  9626  zfcndun  9637  zfcndpow  9638  zfcndinf  9640  zfcndac  9641  fpwwe2lem12  9663  axgroth3  9853  axgroth4  9854  nqereu  9951  mdetunilem9  20650  madugsum  20673  neiptopnei  21163  2ndc1stc  21481  nrmr0reg  21779  alexsubALTlem4  22080  xrsmopn  22841  itg2cn  23756  itgcn  23835  sqff1o  25135  dya2iocuni  30686  bnj849  31334  erdsze  31523  untsucf  31926  untangtr  31930  dfon2lem3  32027  dfon2lem6  32030  dfon2lem7  32031  dfon2  32034  axextdist  32042  distel  32046  neibastop2lem  32693  bj-elequ12  33006  bj-axsep  33130  bj-nalset  33131  bj-zfpow  33132  bj-nfeel2  33172  bj-ru0  33265  prtlem5  34668  ax12el  34750  pw2f1ocnv  38130  aomclem8  38157  lcosslsp  42752
  Copyright terms: Public domain W3C validator