ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eleq1w GIF version

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.
StepHypRef Expression
1 equequ2 1657 . . . 4 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
21anbi1d 456 . . 3 (𝑥 = 𝑦 → ((𝑧 = 𝑥𝑧𝐴) ↔ (𝑧 = 𝑦𝑧𝐴)))
32exbidv 1764 . 2 (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥𝑧𝐴) ↔ ∃𝑧(𝑧 = 𝑦𝑧𝐴)))
4 df-clel 2096 . 2 (𝑥𝐴 ↔ ∃𝑧(𝑧 = 𝑥𝑧𝐴))
5 df-clel 2096 . 2 (𝑦𝐴 ↔ ∃𝑧(𝑧 = 𝑦𝑧𝐴))
63, 4, 53bitr4g 222 1 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator