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

Theorem elequ1 1995
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 1994 . 2 (𝑥 = 𝑦 → (𝑥𝑧𝑦𝑧))
2 ax8 1994 . . 3 (𝑦 = 𝑥 → (𝑦𝑧𝑥𝑧))
32equcoms 1945 . 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 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703
This theorem is referenced by:  cleljust  1996  ax12wdemo  2010  cleljustALT  2183  cleljustALT2  2184  dveel1  2368  axc14  2370  elsb3  2432  axsep  4771  nalset  4786  zfpow  4835  zfun  6935  tz7.48lem  7521  unxpdomlem1  8149  pssnn  8163  zfinf  8521  aceq0  8926  dfac3  8929  dfac5lem2  8932  dfac5lem3  8933  dfac2a  8937  zfac  9267  nd1  9394  axextnd  9398  axrepndlem1  9399  axrepndlem2  9400  axunndlem1  9402  axunnd  9403  axpowndlem2  9405  axpowndlem3  9406  axpowndlem4  9407  axregndlem1  9409  axregnd  9411  zfcndun  9422  zfcndpow  9423  zfcndinf  9425  zfcndac  9426  fpwwe2lem12  9448  axgroth3  9638  axgroth4  9639  nqereu  9736  mdetunilem9  20407  madugsum  20430  neiptopnei  20917  2ndc1stc  21235  nrmr0reg  21533  alexsubALTlem4  21835  xrsmopn  22596  itg2cn  23511  itgcn  23590  sqff1o  24889  dya2iocuni  30319  bnj849  30969  erdsze  31158  untsucf  31561  untangtr  31565  dfon2lem3  31664  dfon2lem6  31667  dfon2lem7  31668  dfon2  31671  axextdist  31679  distel  31683  neibastop2lem  32330  bj-elequ12  32643  bj-axsep  32768  bj-nalset  32769  bj-zfpow  32770  bj-nfeel2  32812  bj-ru0  32907  prtlem5  33963  ax12el  34046  pw2f1ocnv  37423  aomclem8  37450  lcosslsp  41992
  Copyright terms: Public domain W3C validator