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

Step	Hyp	Ref	Expression
1		ax8 2113	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
2		ax8 2113	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
3	2	equcoms 2024	. 2 ⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
4	1, 3	impbid 211	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧))

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  2362  cleljustALT2  2363  dveel1  2461  axc14  2463  sbralie  3355  unissb  4944  dftr2c  5269  axsepgfromrep  5298  nalset  5314  zfpow  5365  dtruALT2  5369  el  5438  dtruOLD  5442  zfun  7726  tz7.48lem  8441  coflton  8670  pssnn  9168  unxpdomlem1  9250  pssnnOLD  9265  zfinf  9634  aceq1  10112  aceq0  10113  aceq2  10114  dfac3  10116  dfac5lem2  10119  dfac5lem3  10120  dfac2a  10124  kmlem4  10148  zfac  10455  nd1  10582  axextnd  10586  axrepndlem1  10587  axrepndlem2  10588  axunndlem1  10590  axunnd  10591  axpowndlem2  10593  axpowndlem3  10594  axpowndlem4  10595  axregndlem1  10597  axregnd  10599  zfcndun  10610  zfcndpow  10611  zfcndinf  10613  zfcndac  10614  fpwwe2lem11  10636  axgroth3  10826  axgroth4  10827  nqereu  10924  mdetunilem9  22122  madugsum  22145  neiptopnei  22636  2ndc1stc  22955  nrmr0reg  23253  alexsubALTlem4  23554  xrsmopn  24328  itg2cn  25281  itgcn  25362  sqff1o  26686  dya2iocuni  33313  bnj849  33967  fineqvrep  34126  erdsze  34224  untsucf  34710  untangtr  34714  dfon2lem3  34788  dfon2lem6  34791  dfon2lem7  34792  dfon2  34795  axextdist  34802  distel  34806  neibastop2lem  35293  bj-elequ12  35604  bj-nfeel2  35781  bj-ru0  35871  prtlem5  37778  prtlem13  37786  prtlem16  37787  ax12el  37860  pw2f1ocnv  41824  aomclem8  41851  onsupmaxb  42036  grumnud  43093  lcosslsp  47167