Theorem elequ1 2116

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

Syntax hints:   → wi 4   ↔ wb 206

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 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780

This theorem is referenced by:  elsb1  2117  cleljust  2118  elequ12  2127  ru0  2128  ax12wdemo  2136  cleljustALT  2362  cleljustALT2  2363  dveel1  2459  axc14  2461  sbralie  3317  sbralieOLD  3319  unissb  4893  dftr2c  5205  axsepgfromrep  5236  nalset  5255  zfpow  5308  dtruALT2  5312  el  5384  dtruOLD  5388  zfun  7676  tz7.48lem  8370  coflton  8596  pssnn  9092  unxpdomlem1  9155  elirrv  9508  zfinf  9554  aceq1  10030  aceq0  10031  aceq2  10032  dfac3  10034  dfac5lem2  10037  dfac5lem3  10038  dfac2a  10043  kmlem4  10067  zfac  10373  nd1  10500  axextnd  10504  axrepndlem1  10505  axrepndlem2  10506  axunndlem1  10508  axunnd  10509  axpowndlem2  10511  axpowndlem3  10512  axpowndlem4  10513  axregndlem1  10515  axregnd  10517  zfcndun  10528  zfcndpow  10529  zfcndinf  10531  zfcndac  10532  fpwwe2lem11  10554  axgroth3  10744  axgroth4  10745  nqereu  10842  mdetunilem9  22523  madugsum  22546  neiptopnei  23035  2ndc1stc  23354  nrmr0reg  23652  alexsubALTlem4  23953  xrsmopn  24717  itg2cn  25680  itgcn  25762  sqff1o  27108  dya2iocuni  34250  bnj849  34891  axnulg  35058  axreg  35061  fineqvrep  35069  erdsze  35174  untsucf  35682  untangtr  35686  dfon2lem3  35758  dfon2lem6  35761  dfon2lem7  35762  dfon2  35765  axextdist  35772  distel  35776  neibastop2lem  36333  bj-nfeel2  36827  prtlem5  38838  prtlem13  38846  prtlem16  38847  ax12el  38920  pw2f1ocnv  43010  aomclem8  43034  onsupmaxb  43212  grumnud  44259  dfnbgr6  47842  lcosslsp  48424