Theorem elequ1 2114

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 2113	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
2		ax8 2113	. . 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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783

This theorem is referenced by:  elsb1  2115  cleljust  2116  ax12wdemo  2132  cleljustALT  2362  cleljustALT2  2363  dveel1  2461  axc14  2463  sbralie  3355  unissb  4944  dftr2c  5269  axsepgfromrep  5298  nalset  5314  zfpow  5365  dtruALT2  5369  el  5438  dtruOLD  5442  zfun  7726  tz7.48lem  8441  coflton  8670  pssnn  9168  unxpdomlem1  9250  pssnnOLD  9265  zfinf  9634  aceq1  10112  aceq0  10113  aceq2  10114  dfac3  10116  dfac5lem2  10119  dfac5lem3  10120  dfac2a  10124  kmlem4  10148  zfac  10455  nd1  10582  axextnd  10586  axrepndlem1  10587  axrepndlem2  10588  axunndlem1  10590  axunnd  10591  axpowndlem2  10593  axpowndlem3  10594  axpowndlem4  10595  axregndlem1  10597  axregnd  10599  zfcndun  10610  zfcndpow  10611  zfcndinf  10613  zfcndac  10614  fpwwe2lem11  10636  axgroth3  10826  axgroth4  10827  nqereu  10924  mdetunilem9  22122  madugsum  22145  neiptopnei  22636  2ndc1stc  22955  nrmr0reg  23253  alexsubALTlem4  23554  xrsmopn  24328  itg2cn  25281  itgcn  25362  sqff1o  26686  dya2iocuni  33282  bnj849  33936  fineqvrep  34095  erdsze  34193  untsucf  34679  untangtr  34683  dfon2lem3  34757  dfon2lem6  34760  dfon2lem7  34761  dfon2  34764  axextdist  34771  distel  34775  neibastop2lem  35245  bj-elequ12  35556  bj-nfeel2  35733  bj-ru0  35823  prtlem5  37730  prtlem13  37738  prtlem16  37739  ax12el  37812  pw2f1ocnv  41776  aomclem8  41803  onsupmaxb  41988  grumnud  43045  lcosslsp  47119