Theorem elequ1 2110

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

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1968  ax-7 2008  ax-8 2105

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1779

This theorem is referenced by:  elsb1  2111  cleljust  2112  ax12wdemo  2128  cleljustALT  2359  cleljustALT2  2360  dveel1  2458  axc14  2460  unissb  4878  dftr2c  5200  axsepgfromrep  5229  nalset  5245  zfpow  5297  dtruALT2  5301  el  5369  dtruOLD  5371  zfun  7622  tz7.48lem  8307  pssnn  8998  unxpdomlem1  9080  pssnnOLD  9095  zfinf  9455  aceq1  9933  aceq0  9934  aceq2  9935  dfac3  9937  dfac5lem2  9940  dfac5lem3  9941  dfac2a  9945  kmlem4  9969  zfac  10276  nd1  10403  axextnd  10407  axrepndlem1  10408  axrepndlem2  10409  axunndlem1  10411  axunnd  10412  axpowndlem2  10414  axpowndlem3  10415  axpowndlem4  10416  axregndlem1  10418  axregnd  10420  zfcndun  10431  zfcndpow  10432  zfcndinf  10434  zfcndac  10435  fpwwe2lem11  10457  axgroth3  10647  axgroth4  10648  nqereu  10745  mdetunilem9  21832  madugsum  21855  neiptopnei  22346  2ndc1stc  22665  nrmr0reg  22963  alexsubALTlem4  23264  xrsmopn  24038  itg2cn  24991  itgcn  25072  sqff1o  26394  dya2iocuni  32346  bnj849  33001  fineqvrep  33160  erdsze  33260  untsucf  33747  untangtr  33751  dfon2lem3  33855  dfon2lem6  33858  dfon2lem7  33859  dfon2  33862  axextdist  33869  distel  33873  neibastop2lem  34608  bj-elequ12  34919  bj-nfeel2  35096  bj-ru0  35189  prtlem5  37084  prtlem13  37092  prtlem16  37093  ax12el  37166  pw2f1ocnv  41068  aomclem8  41095  grumnud  42130  lcosslsp  46036