Theorem elequ1 2148

Description: An identity law for the non-logical predicate. (Contributed by NM, 30-Jun-1993.)

Assertion

Ref	Expression
elequ1	⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧))

Proof of Theorem elequ1

Step	Hyp	Ref	Expression
1		ax8 2147	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
2		ax8 2147	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
3	2	equcoms 2039	. 2 ⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
4	1, 3	impbid 214	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧))

Syntax hints:   → wi 4   ↔ wb 208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799

This theorem is referenced by:  elsb1  2149  cleljust  2150  elequ12  2159  ru0  2160  ax12wdemo  2168  cleljustALT  2394  cleljustALT2  2395  dveel1  2491  axc14  2493  sbralie  3339  sbralieOLD  3341  unissb  4898  dftr2c  5209  axsepgfromrep  5243  exnelv  5262  nalsetOLD  5264  zfpow  5322  dtruALT2  5326  elOLD  5405  zfun  7715  tz7.48lem  8407  coflton  8636  pssnn  9133  unxpdomlem1  9196  elirrv  9542  elirrvOLD  9543  zfinf  9591  aceq1  10070  aceq0  10071  aceq2  10072  dfac3  10074  dfac5lem2  10077  dfac5lem3  10078  dfac2a  10083  kmlem4  10107  zfac  10414  nd1  10542  axextnd  10546  axrepndlem1  10547  axrepndlem2  10548  axunndlem1  10550  axunnd  10551  axpowndlem2  10553  axpowndlem3  10554  axpowndlem4  10555  axregndlem1  10557  axregnd  10559  zfcndun  10570  zfcndpow  10571  zfcndinf  10573  zfcndac  10574  fpwwe2lem11  10596  axgroth3  10786  axgroth4  10787  nqereu  10884  mdetunilem9  22660  madugsum  22683  neiptopnei  23172  2ndc1stc  23491  nrmr0reg  23789  alexsubALTlem4  24090  xrsmopn  24853  itg2cn  25805  itgcn  25887  sqff1o  27223  dya2iocuni  34541  bnj849  35184  axprALT2  35369  fineqvrep  35374  axreg  35387  axsepg2  35400  axsepg4  35403  axnulg  35405  axpowg  35406  erdsze  35516  untsucf  36024  untangtr  36028  dfon2lem3  36097  dfon2lem6  36100  dfon2lem7  36101  dfon2  36104  axextdist  36111  distel  36115  nmulprop  36504  neibastop2lem  36684  axtco1  36797  axtco2  36798  axtco1from2  36799  axtcond  36802  axuntco  36803  axnulregtco  36804  regsfromregtco  36862  regsfromsetind  36863  mh-prprimbi  36867  mh-unprimbi  36868  mh-regprimbi  36869  mh-infprim2bi  36871  bj-nfeel2  37303  bj-axseprep  37523  prtlem5  39448  prtlem13  39456  prtlem16  39457  ax12el  39530  pw2f1ocnv  43578  aomclem8  43602  onsupmaxb  43780  grumnud  44826  dfnbgr6  48443  lcosslsp  49024