Theorem elequ1 2120

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 2119	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
2		ax8 2119	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
3	2	equcoms 2026	. 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 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780

This theorem is referenced by:  elsb3  2121  cleljust  2122  ax12wdemo  2138  cleljustALT  2381  cleljustALT2  2382  dveel1  2483  axc14  2485  axsepgfromrep  5204  nalset  5220  zfpow  5270  zfun  7465  tz7.48lem  8080  unxpdomlem1  8725  pssnn  8739  zfinf  9105  aceq1  9546  aceq0  9547  aceq2  9548  dfac3  9550  dfac5lem2  9553  dfac5lem3  9554  dfac2a  9558  kmlem4  9582  zfac  9885  nd1  10012  axextnd  10016  axrepndlem1  10017  axrepndlem2  10018  axunndlem1  10020  axunnd  10021  axpowndlem2  10023  axpowndlem3  10024  axpowndlem4  10025  axregndlem1  10027  axregnd  10029  zfcndun  10040  zfcndpow  10041  zfcndinf  10043  zfcndac  10044  fpwwe2lem12  10066  axgroth3  10256  axgroth4  10257  nqereu  10354  mdetunilem9  21232  madugsum  21255  neiptopnei  21743  2ndc1stc  22062  nrmr0reg  22360  alexsubALTlem4  22661  xrsmopn  23423  itg2cn  24367  itgcn  24446  sqff1o  25762  dya2iocuni  31545  bnj849  32201  erdsze  32453  untsucf  32940  untangtr  32944  dfon2lem3  33034  dfon2lem6  33037  dfon2lem7  33038  dfon2  33041  axextdist  33048  distel  33052  neibastop2lem  33712  bj-elequ12  34016  bj-nfeel2  34182  bj-ru0  34257  prtlem5  36000  prtlem13  36008  prtlem16  36009  ax12el  36082  pw2f1ocnv  39640  aomclem8  39667  grumnud  40628  lcosslsp  44500