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

Theorem elequ1 1996
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 1995 . 2 (𝑥 = 𝑦 → (𝑥𝑧𝑦𝑧))
2 ax8 1995 . . 3 (𝑦 = 𝑥 → (𝑦𝑧𝑥𝑧))
32equcoms 1946 . 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 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1704
This theorem is referenced by:  cleljust  1997  ax12wdemo  2011  cleljustALT  2184  cleljustALT2  2185  dveel1  2369  axc14  2371  elsb3  2433  axsep  4778  nalset  4793  zfpow  4842  zfun  6947  tz7.48lem  7533  unxpdomlem1  8161  pssnn  8175  zfinf  8533  aceq0  8938  dfac3  8941  dfac5lem2  8944  dfac5lem3  8945  dfac2a  8949  zfac  9279  nd1  9406  axextnd  9410  axrepndlem1  9411  axrepndlem2  9412  axunndlem1  9414  axunnd  9415  axpowndlem2  9417  axpowndlem3  9418  axpowndlem4  9419  axregndlem1  9421  axregnd  9423  zfcndun  9434  zfcndpow  9435  zfcndinf  9437  zfcndac  9438  fpwwe2lem12  9460  axgroth3  9650  axgroth4  9651  nqereu  9748  mdetunilem9  20420  madugsum  20443  neiptopnei  20930  2ndc1stc  21248  nrmr0reg  21546  alexsubALTlem4  21848  xrsmopn  22609  itg2cn  23524  itgcn  23603  sqff1o  24902  dya2iocuni  30330  bnj849  30980  erdsze  31169  untsucf  31572  untangtr  31576  dfon2lem3  31674  dfon2lem6  31677  dfon2lem7  31678  dfon2  31681  axextdist  31689  distel  31693  neibastop2lem  32339  bj-elequ12  32652  bj-axsep  32777  bj-nalset  32778  bj-zfpow  32779  bj-nfeel2  32821  bj-ru0  32916  prtlem5  33971  ax12el  34053  pw2f1ocnv  37430  aomclem8  37457  lcosslsp  41998
  Copyright terms: Public domain W3C validator