Theorem eleq1w 2200

Description: Weaker version of eleq1 2202 (but more general than elequ1 1690) not depending on ax-ext 2121 nor df-cleq 2132. (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 2135	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴))
5		df-clel 2135	. 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 2135

This theorem is referenced by:  clelsb3f  2285  dfdif3  3186  dfss4st  3309  abn0m  3388  r19.2m  3449  cbvmptf  4022  iinexgm  4079  xpiindim  4676  cnviinm  5080  iinerm  6501  ixpiinm  6618  ixpsnf1o  6630  mapsnen  6705  enumctlemm  6999  exmidomni  7014  fodjum  7018  suplocexprlemmu  7526  suplocsr  7617  axpre-suploc  7710  iseqf1olemqk  10267  seq3f1olemqsum  10273  summodclem2  11151  summodc  11152  zsumdc  11153  fsum3  11156  isumz  11158  isumss  11160  fisumss  11161  isumss2  11162  fsum3cvg2  11163  fsumsersdc  11164  fsum3ser  11166  fsumsplit  11176  fsumsplitf  11177  isumlessdc  11265  prodfdivap  11316  cbvprod  11327  prodrbdclem  11340  prodmodclem2  11346  prodmodc  11347  neipsm  12323  dedekindeulemub  12765  dedekindeulemloc  12766  dedekindeulemlub  12767  suplociccex  12772  dedekindicclemub  12774  dedekindicclemloc  12775  dedekindicclemlub  12776  limcimo  12803  nninfalllemn  13202