Theorem elequ1 2115

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 2114	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
2		ax8 2114	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
3	2	equcoms 2019	. 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 2007  ax-8 2110

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

This theorem is referenced by:  elsb1  2116  cleljust  2117  elequ12  2126  ru0  2127  ax12wdemo  2135  cleljustALT  2366  cleljustALT2  2367  dveel1  2465  axc14  2467  sbralie  3337  unissb  4915  dftr2c  5232  axsepgfromrep  5264  nalset  5283  zfpow  5336  dtruALT2  5340  el  5412  dtruOLD  5416  zfun  7730  tz7.48lem  8455  coflton  8683  pssnn  9182  unxpdomlem1  9258  zfinf  9653  aceq1  10131  aceq0  10132  aceq2  10133  dfac3  10135  dfac5lem2  10138  dfac5lem3  10139  dfac2a  10144  kmlem4  10168  zfac  10474  nd1  10601  axextnd  10605  axrepndlem1  10606  axrepndlem2  10607  axunndlem1  10609  axunnd  10610  axpowndlem2  10612  axpowndlem3  10613  axpowndlem4  10614  axregndlem1  10616  axregnd  10618  zfcndun  10629  zfcndpow  10630  zfcndinf  10632  zfcndac  10633  fpwwe2lem11  10655  axgroth3  10845  axgroth4  10846  nqereu  10943  mdetunilem9  22558  madugsum  22581  neiptopnei  23070  2ndc1stc  23389  nrmr0reg  23687  alexsubALTlem4  23988  xrsmopn  24752  itg2cn  25716  itgcn  25798  sqff1o  27144  dya2iocuni  34315  bnj849  34956  axnulg  35123  fineqvrep  35126  erdsze  35224  untsucf  35727  untangtr  35731  dfon2lem3  35803  dfon2lem6  35806  dfon2lem7  35807  dfon2  35810  axextdist  35817  distel  35821  neibastop2lem  36378  bj-nfeel2  36872  prtlem5  38878  prtlem13  38886  prtlem16  38887  ax12el  38960  pw2f1ocnv  43061  aomclem8  43085  onsupmaxb  43263  grumnud  44310  dfnbgr6  47870  lcosslsp  48414