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

Theorem elequ1 1983
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 1982 . 2 (𝑥 = 𝑦 → (𝑥𝑧𝑦𝑧))
2 ax8 1982 . . 3 (𝑦 = 𝑥 → (𝑦𝑧𝑥𝑧))
32equcoms 1933 . 2 (𝑥 = 𝑦 → (𝑦𝑧𝑥𝑧))
41, 3impbid 200 1 (𝑥 = 𝑦 → (𝑥𝑧𝑦𝑧))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695
This theorem is referenced by:  cleljust  1984  ax12wdemo  1998  cleljustALT  2168  cleljustALT2  2169  dveel1  2354  axc14  2356  elsb3  2418  axsep  4699  nalset  4715  zfpow  4762  zfun  6822  tz7.48lem  7397  unxpdomlem1  8023  pssnn  8037  zfinf  8393  aceq0  8798  dfac3  8801  dfac5lem2  8804  dfac5lem3  8805  dfac2a  8809  zfac  9139  nd1  9262  axextnd  9266  axrepndlem1  9267  axrepndlem2  9268  axunndlem1  9270  axunnd  9271  axpowndlem2  9273  axpowndlem3  9274  axpowndlem4  9275  axregndlem1  9277  axregnd  9279  zfcndun  9290  zfcndpow  9291  zfcndinf  9293  zfcndac  9294  fpwwe2lem12  9316  axgroth3  9506  axgroth4  9507  nqereu  9604  mdetunilem9  20184  madugsum  20207  neiptopnei  20685  2ndc1stc  21003  nrmr0reg  21301  alexsubALTlem4  21603  xrsmopn  22352  itg2cn  23250  itgcn  23329  sqff1o  24622  dya2iocuni  29475  bnj849  30052  erdsze  30241  untsucf  30644  untangtr  30648  dfon2lem3  30737  dfon2lem6  30740  dfon2lem7  30741  dfon2  30744  axextdist  30752  distel  30756  neibastop2lem  31328  bj-elequ12  31658  bj-axsep  31791  bj-nalset  31792  bj-zfpow  31793  bj-ru0  31924  prtlem5  32962  ax12el  33045  pw2f1ocnv  36422  aomclem8  36449  lcosslsp  42020
  Copyright terms: Public domain W3C validator