Theorem eleq1w 2198

Description: Weaker version of eleq1 2200 (but more general than elequ1 1690) not depending on ax-ext 2119 nor df-cleq 2130. (Contributed by BJ, 24-Jun-2019.)

Assertion

Ref	Expression
eleq1w	⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

Proof of Theorem eleq1w

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		equequ2 1689	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
2	1	anbi1d 460	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ (𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
3	2	exbidv 1797	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
4		df-clel 2133	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴))
5		df-clel 2133	. 2 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴))
6	3, 4, 5	3bitr4g 222	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∃wex 1468   ∈ wcel 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-clel 2133

This theorem is referenced by:  clelsb3f  2283  dfdif3  3181  dfss4st  3304  abn0m  3383  r19.2m  3444  cbvmptf  4017  iinexgm  4074  xpiindim  4671  cnviinm  5075  iinerm  6494  ixpiinm  6611  ixpsnf1o  6623  mapsnen  6698  enumctlemm  6992  exmidomni  7007  fodjum  7011  suplocexprlemmu  7519  suplocsr  7610  axpre-suploc  7703  iseqf1olemqk  10260  seq3f1olemqsum  10266  summodclem2  11144  summodc  11145  zsumdc  11146  fsum3  11149  isumz  11151  isumss  11153  fisumss  11154  isumss2  11155  fsum3cvg2  11156  fsumsersdc  11157  fsum3ser  11159  fsumsplit  11169  fsumsplitf  11170  isumlessdc  11258  prodfdivap  11309  cbvprod  11320  prodrbdclem  11333  neipsm  12312  dedekindeulemub  12754  dedekindeulemloc  12755  dedekindeulemlub  12756  suplociccex  12761  dedekindicclemub  12763  dedekindicclemloc  12764  dedekindicclemlub  12765  limcimo  12792  nninfalllemn  13191