Theorem eleq1w 2160

Description: Weaker version of eleq1 2162 (but more general than elequ1 1658) not depending on ax-ext 2082 nor df-cleq 2093. (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 1657	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
2	1	anbi1d 456	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ (𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
3	2	exbidv 1764	. 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)))
4		df-clel 2096	. 2 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴))
5		df-clel 2096	. 2 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴))
6	3, 4, 5	3bitr4g 222	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482

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

This theorem is referenced by:  clelsb3f  2244  dfdif3  3133  dfss4st  3256  abn0m  3335  r19.2m  3396  cbvmptf  3962  iinexgm  4019  xpiindim  4614  cnviinm  5016  iinerm  6431  ixpiinm  6548  ixpsnf1o  6560  mapsnen  6635  enumctlemm  6913  exmidomni  6926  fodjum  6930  iseqf1olemqk  10108  seq3f1olemqsum  10114  summodclem2  10990  summodc  10991  zsumdc  10992  fsum3  10995  isumz  10997  isumss  10999  fisumss  11000  isumss2  11001  fsum3cvg2  11002  fsumsersdc  11003  fsum3ser  11005  fsumsplit  11015  fsumsplitf  11016  isumlessdc  11104  neipsm  12105  limcimo  12514  nninfalllemn  12786