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

Theorem elequ1 2114
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 2113 . 2 (𝑥 = 𝑦 → (𝑥𝑧𝑦𝑧))
2 ax8 2113 . . 3 (𝑦 = 𝑥 → (𝑦𝑧𝑥𝑧))
32equcoms 2024 . 2 (𝑥 = 𝑦 → (𝑦𝑧𝑥𝑧))
41, 3impbid 211 1 (𝑥 = 𝑦 → (𝑥𝑧𝑦𝑧))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783
This theorem is referenced by:  elsb1  2115  cleljust  2116  ax12wdemo  2132  cleljustALT  2361  cleljustALT2  2362  dveel1  2460  axc14  2462  unissb  4905  dftr2c  5230  axsepgfromrep  5259  nalset  5275  zfpow  5326  dtruALT2  5330  el  5399  dtruOLD  5403  zfun  7678  tz7.48lem  8392  coflton  8622  pssnn  9119  unxpdomlem1  9201  pssnnOLD  9216  zfinf  9582  aceq1  10060  aceq0  10061  aceq2  10062  dfac3  10064  dfac5lem2  10067  dfac5lem3  10068  dfac2a  10072  kmlem4  10096  zfac  10403  nd1  10530  axextnd  10534  axrepndlem1  10535  axrepndlem2  10536  axunndlem1  10538  axunnd  10539  axpowndlem2  10541  axpowndlem3  10542  axpowndlem4  10543  axregndlem1  10545  axregnd  10547  zfcndun  10558  zfcndpow  10559  zfcndinf  10561  zfcndac  10562  fpwwe2lem11  10584  axgroth3  10774  axgroth4  10775  nqereu  10872  mdetunilem9  21985  madugsum  22008  neiptopnei  22499  2ndc1stc  22818  nrmr0reg  23116  alexsubALTlem4  23417  xrsmopn  24191  itg2cn  25144  itgcn  25225  sqff1o  26547  dya2iocuni  32923  bnj849  33577  fineqvrep  33736  erdsze  33836  untsucf  34321  untangtr  34325  dfon2lem3  34399  dfon2lem6  34402  dfon2lem7  34403  dfon2  34406  axextdist  34413  distel  34417  neibastop2lem  34861  bj-elequ12  35172  bj-nfeel2  35349  bj-ru0  35442  prtlem5  37351  prtlem13  37359  prtlem16  37360  ax12el  37433  pw2f1ocnv  41390  aomclem8  41417  onsupmaxb  41602  grumnud  42640  lcosslsp  46593
  Copyright terms: Public domain W3C validator