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

Theorem elequ1 1984
 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 1983 . 2 (𝑥 = 𝑦 → (𝑥𝑧𝑦𝑧))
2 ax8 1983 . . 3 (𝑦 = 𝑥 → (𝑦𝑧𝑥𝑧))
32equcoms 1934 . 2 (𝑥 = 𝑦 → (𝑦𝑧𝑥𝑧))
41, 3impbid 201 1 (𝑥 = 𝑦 → (𝑥𝑧𝑦𝑧))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696 This theorem is referenced by:  cleljust  1985  ax12wdemo  1999  cleljustALT  2173  cleljustALT2  2174  dveel1  2358  axc14  2360  elsb3  2422  axsep  4708  nalset  4723  zfpow  4770  zfun  6848  tz7.48lem  7423  unxpdomlem1  8049  pssnn  8063  zfinf  8419  aceq0  8824  dfac3  8827  dfac5lem2  8830  dfac5lem3  8831  dfac2a  8835  zfac  9165  nd1  9288  axextnd  9292  axrepndlem1  9293  axrepndlem2  9294  axunndlem1  9296  axunnd  9297  axpowndlem2  9299  axpowndlem3  9300  axpowndlem4  9301  axregndlem1  9303  axregnd  9305  zfcndun  9316  zfcndpow  9317  zfcndinf  9319  zfcndac  9320  fpwwe2lem12  9342  axgroth3  9532  axgroth4  9533  nqereu  9630  mdetunilem9  20245  madugsum  20268  neiptopnei  20746  2ndc1stc  21064  nrmr0reg  21362  alexsubALTlem4  21664  xrsmopn  22423  itg2cn  23336  itgcn  23415  sqff1o  24708  dya2iocuni  29672  bnj849  30249  erdsze  30438  untsucf  30841  untangtr  30845  dfon2lem3  30934  dfon2lem6  30937  dfon2lem7  30938  dfon2  30941  axextdist  30949  distel  30953  neibastop2lem  31525  bj-elequ12  31855  bj-axsep  31981  bj-nalset  31982  bj-zfpow  31983  bj-ru0  32124  prtlem5  33162  ax12el  33245  pw2f1ocnv  36622  aomclem8  36649  lcosslsp  42021
 Copyright terms: Public domain W3C validator