Theorem elequ1 2126

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

Syntax hints:   → wi 4   ↔ wb 207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787

This theorem is referenced by:  elsb1  2127  cleljust  2128  elequ12  2137  ru0  2138  ax12wdemo  2146  cleljustALT  2372  cleljustALT2  2373  dveel1  2469  axc14  2471  sbralie  3318  sbralieOLD  3320  unissb  4878  dftr2c  5189  axsepgfromrep  5223  exnelv  5242  nalsetOLD  5244  zfpow  5302  dtruALT2  5306  elOLD  5385  zfun  7686  tz7.48lem  8377  coflton  8604  pssnn  9100  unxpdomlem1  9163  elirrv  9509  elirrvOLD  9510  zfinf  9558  aceq1  10037  aceq0  10038  aceq2  10039  dfac3  10041  dfac5lem2  10044  dfac5lem3  10045  dfac2a  10050  kmlem4  10074  zfac  10380  nd1  10508  axextnd  10512  axrepndlem1  10513  axrepndlem2  10514  axunndlem1  10516  axunnd  10517  axpowndlem2  10519  axpowndlem3  10520  axpowndlem4  10521  axregndlem1  10523  axregnd  10525  zfcndun  10536  zfcndpow  10537  zfcndinf  10539  zfcndac  10540  fpwwe2lem11  10562  axgroth3  10752  axgroth4  10753  nqereu  10850  mdetunilem9  22610  madugsum  22633  neiptopnei  23122  2ndc1stc  23441  nrmr0reg  23739  alexsubALTlem4  24040  xrsmopn  24803  itg2cn  25755  itgcn  25837  sqff1o  27170  dya2iocuni  34474  bnj849  35114  axprALT2  35297  fineqvrep  35302  axreg  35315  axsepg2  35328  axsepg4  35331  axnulg  35333  axpowg  35334  erdsze  35437  untsucf  35945  untangtr  35949  dfon2lem3  36018  dfon2lem6  36021  dfon2lem7  36022  dfon2  36025  axextdist  36032  distel  36036  neibastop2lem  36595  axtco1  36708  axtco2  36709  axtco1from2  36710  axtcond  36713  axuntco  36714  axnulregtco  36715  regsfromregtco  36773  regsfromsetind  36774  mh-prprimbi  36778  mh-unprimbi  36779  mh-regprimbi  36780  mh-infprim2bi  36782  bj-nfeel2  37214  bj-axseprep  37434  prtlem5  39359  prtlem13  39367  prtlem16  39368  ax12el  39441  pw2f1ocnv  43489  aomclem8  43513  onsupmaxb  43691  grumnud  44737  dfnbgr6  48355  lcosslsp  48936