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 2024	. 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 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784

This theorem is referenced by:  elsb1  2116  cleljust  2117  ax12wdemo  2133  cleljustALT  2362  cleljustALT2  2363  dveel1  2461  axc14  2463  axsepgfromrep  5216  nalset  5232  zfpow  5284  dtru  5288  zfun  7567  tz7.48lem  8242  pssnn  8913  unxpdomlem1  8956  pssnnOLD  8969  zfinf  9327  aceq1  9804  aceq0  9805  aceq2  9806  dfac3  9808  dfac5lem2  9811  dfac5lem3  9812  dfac2a  9816  kmlem4  9840  zfac  10147  nd1  10274  axextnd  10278  axrepndlem1  10279  axrepndlem2  10280  axunndlem1  10282  axunnd  10283  axpowndlem2  10285  axpowndlem3  10286  axpowndlem4  10287  axregndlem1  10289  axregnd  10291  zfcndun  10302  zfcndpow  10303  zfcndinf  10305  zfcndac  10306  fpwwe2lem11  10328  axgroth3  10518  axgroth4  10519  nqereu  10616  mdetunilem9  21677  madugsum  21700  neiptopnei  22191  2ndc1stc  22510  nrmr0reg  22808  alexsubALTlem4  23109  xrsmopn  23881  itg2cn  24833  itgcn  24914  sqff1o  26236  dya2iocuni  32150  bnj849  32805  fineqvrep  32964  erdsze  33064  untsucf  33551  untangtr  33555  dfon2lem3  33667  dfon2lem6  33670  dfon2lem7  33671  dfon2  33674  axextdist  33681  distel  33685  neibastop2lem  34476  bj-elequ12  34787  bj-nfeel2  34965  bj-ru0  35058  prtlem5  36801  prtlem13  36809  prtlem16  36810  ax12el  36883  pw2f1ocnv  40775  aomclem8  40802  grumnud  41793  lcosslsp  45667