Theorem elequ1 2086

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

Syntax hints:   → wi 4   ↔ wb 207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1760

This theorem is referenced by:  elsb3  2087  cleljust  2088  ax12wdemo  2104  cleljustALT  2337  cleljustALT2  2338  dveel1  2439  axc14  2441  axsepgfromrep  5086  nalset  5102  zfpow  5151  zfun  7311  tz7.48lem  7919  unxpdomlem1  8558  pssnn  8572  zfinf  8937  aceq1  9378  aceq0  9379  aceq2  9380  dfac3  9382  dfac5lem2  9385  dfac5lem3  9386  dfac2a  9390  kmlem4  9414  zfac  9717  nd1  9844  axextnd  9848  axrepndlem1  9849  axrepndlem2  9850  axunndlem1  9852  axunnd  9853  axpowndlem2  9855  axpowndlem3  9856  axpowndlem4  9857  axregndlem1  9859  axregnd  9861  zfcndun  9872  zfcndpow  9873  zfcndinf  9875  zfcndac  9876  fpwwe2lem12  9898  axgroth3  10088  axgroth4  10089  nqereu  10186  mdetunilem9  20901  madugsum  20924  neiptopnei  21412  2ndc1stc  21731  nrmr0reg  22029  alexsubALTlem4  22330  xrsmopn  23091  itg2cn  24035  itgcn  24114  sqff1o  25429  dya2iocuni  31114  bnj849  31769  erdsze  32013  untsucf  32489  untangtr  32493  dfon2lem3  32583  dfon2lem6  32586  dfon2lem7  32587  dfon2  32590  axextdist  32598  distel  32602  neibastop2lem  33262  bj-elequ12  33555  bj-nfeel2  33692  bj-ru0  33770  prtlem5  35477  prtlem13  35485  prtlem16  35486  ax12el  35559  pw2f1ocnv  39070  aomclem8  39097  grumnud  40071  lcosslsp  43927