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

Syntax hints:   → wi 4   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788

This theorem is referenced by:  elsb3  2118  cleljust  2119  ax12wdemo  2135  cleljustALT  2363  cleljustALT2  2364  dveel1  2460  axc14  2462  axsepgfromrep  5190  nalset  5206  zfpow  5259  dtru  5263  zfun  7524  tz7.48lem  8177  pssnn  8846  unxpdomlem1  8882  pssnnOLD  8895  zfinf  9254  aceq1  9731  aceq0  9732  aceq2  9733  dfac3  9735  dfac5lem2  9738  dfac5lem3  9739  dfac2a  9743  kmlem4  9767  zfac  10074  nd1  10201  axextnd  10205  axrepndlem1  10206  axrepndlem2  10207  axunndlem1  10209  axunnd  10210  axpowndlem2  10212  axpowndlem3  10213  axpowndlem4  10214  axregndlem1  10216  axregnd  10218  zfcndun  10229  zfcndpow  10230  zfcndinf  10232  zfcndac  10233  fpwwe2lem11  10255  axgroth3  10445  axgroth4  10446  nqereu  10543  mdetunilem9  21517  madugsum  21540  neiptopnei  22029  2ndc1stc  22348  nrmr0reg  22646  alexsubALTlem4  22947  xrsmopn  23709  itg2cn  24661  itgcn  24742  sqff1o  26064  dya2iocuni  31962  bnj849  32618  fineqvrep  32777  erdsze  32877  untsucf  33364  untangtr  33368  dfon2lem3  33480  dfon2lem6  33483  dfon2lem7  33484  dfon2  33487  axextdist  33494  distel  33498  neibastop2lem  34286  bj-elequ12  34597  bj-nfeel2  34775  bj-ru0  34868  prtlem5  36611  prtlem13  36619  prtlem16  36620  ax12el  36693  pw2f1ocnv  40562  aomclem8  40589  grumnud  41577  lcosslsp  45452