Theorem elequ1 2117

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 2116	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
2		ax8 2116	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
3	2	equcoms 2023	. 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 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112

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

This theorem is referenced by:  elsb3  2118  cleljust  2119  ax12wdemo  2135  cleljustALT  2378  cleljustALT2  2379  dveel1  2480  axc14  2482  axsepgfromrep  5194  nalset  5210  zfpow  5260  zfun  7456  tz7.48lem  8071  unxpdomlem1  8716  pssnn  8730  zfinf  9096  aceq1  9537  aceq0  9538  aceq2  9539  dfac3  9541  dfac5lem2  9544  dfac5lem3  9545  dfac2a  9549  kmlem4  9573  zfac  9876  nd1  10003  axextnd  10007  axrepndlem1  10008  axrepndlem2  10009  axunndlem1  10011  axunnd  10012  axpowndlem2  10014  axpowndlem3  10015  axpowndlem4  10016  axregndlem1  10018  axregnd  10020  zfcndun  10031  zfcndpow  10032  zfcndinf  10034  zfcndac  10035  fpwwe2lem12  10057  axgroth3  10247  axgroth4  10248  nqereu  10345  mdetunilem9  21223  madugsum  21246  neiptopnei  21734  2ndc1stc  22053  nrmr0reg  22351  alexsubALTlem4  22652  xrsmopn  23414  itg2cn  24358  itgcn  24437  sqff1o  25753  dya2iocuni  31536  bnj849  32192  erdsze  32444  untsucf  32931  untangtr  32935  dfon2lem3  33025  dfon2lem6  33028  dfon2lem7  33029  dfon2  33032  axextdist  33039  distel  33043  neibastop2lem  33703  bj-elequ12  34007  bj-nfeel2  34173  bj-ru0  34248  prtlem5  35990  prtlem13  35998  prtlem16  35999  ax12el  36072  pw2f1ocnv  39627  aomclem8  39654  grumnud  40615  lcosslsp  44486