Theorem elequ1 2153

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 2152	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
2		ax8 2152	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
3	2	equcoms 2053	. 2 ⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
4	1, 3	impbid 215	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  elsb1  2154  cleljust  2155  elequ12  2164  ru0  2165  ax12wdemo  2173  cleljustALT  2399  cleljustALT2  2400  dveel1  2496  axc14  2498  sbralie  3345  sbralieOLD  3347  unissb  4911  dftr2c  5226  axsepgfromrep  5260  exnelv  5281  nalsetOLD  5283  zfpow  5342  dtruALT2  5346  el.OLD  5425  zfun  7746  tz7.48lem  8437  coflton  8666  pssnn  9163  unxpdomlem1  9226  elirrv  9569  elirrvOLD  9570  zfinf  9618  aceq1  10120  aceq0  10121  aceq2  10122  dfac3  10124  dfac5lem2  10127  dfac5lem3  10128  dfac2a  10132  kmlem4  10156  zfac  10462  nd1  10590  axextnd  10594  axrepndlem1  10595  axrepndlem2  10596  axunndlem1  10598  axunnd  10599  axpowndlem2  10601  axpowndlem3  10602  axpowndlem4  10603  axregndlem1  10605  axregnd  10607  zfcndun  10618  zfcndpow  10619  zfcndinf  10621  zfcndac  10622  fpwwe2lem11  10644  axgroth3  10834  axgroth4  10835  nqereu  10932  mdetunilem9  22814  madugsum  22837  neiptopnei  23326  2ndc1stc  23645  nrmr0reg  23943  alexsubALTlem4  24244  xrsmopn  25007  itg2cn  25959  itgcn  26041  sqff1o  27383  dya2iocuni  34705  bnj849  35345  axprALT2  35528  fineqvrep  35551  axreg  35564  axsepg2  35577  axsepg4  35580  axnulg  35582  axpowg  35583  erdsze  35715  untsucf  36223  untangtr  36227  dfon2lem3  36296  dfon2lem6  36299  dfon2lem7  36300  dfon2  36303  axextdist  36310  distel  36314  nmulprop  36703  neibastop2lem  36912  axtco1  37025  axtco2  37026  axtco1from2  37027  axtcond  37030  axuntco  37031  axnulregtco  37032  regsfromregtco  37090  regsfromsetind  37091  mh-prprimbi  37095  mh-unprimbi  37096  mh-regprimbi  37097  mh-infprim2bi  37099  bj-nfeel2  37530  bj-axseprep  37752  prtlem5  39675  prtlem13  39683  prtlem16  39684  ax12el  39757  pw2f1ocnv  43805  aomclem8  43829  onsupmaxb  44007  grumnud  45037  dfnbgr6  48663  lcosslsp  49259