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

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.
StepHypRef Expression
1 equequ2 1689 . . . 4 (𝑥 = 𝑦 → (𝑧 = 𝑥𝑧 = 𝑦))
21anbi1d 460 . . 3 (𝑥 = 𝑦 → ((𝑧 = 𝑥𝑧𝐴) ↔ (𝑧 = 𝑦𝑧𝐴)))
32exbidv 1797 . 2 (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥𝑧𝐴) ↔ ∃𝑧(𝑧 = 𝑦𝑧𝐴)))
4 df-clel 2135 . 2 (𝑥𝐴 ↔ ∃𝑧(𝑧 = 𝑥𝑧𝐴))
5 df-clel 2135 . 2 (𝑦𝐴 ↔ ∃𝑧(𝑧 = 𝑦𝑧𝐴))
63, 4, 53bitr4g 222 1 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
 Colors of variables: wff set class 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  cc2  7087  suplocexprlemmu  7538  suplocsr  7629  axpre-suploc  7722  iseqf1olemqk  10279  seq3f1olemqsum  10285  summodclem2  11163  summodc  11164  zsumdc  11165  fsum3  11168  isumz  11170  isumss  11172  fisumss  11173  isumss2  11174  fsum3cvg2  11175  fsumsersdc  11176  fsum3ser  11178  fsumsplit  11188  fsumsplitf  11189  isumlessdc  11277  prodfdivap  11328  cbvprod  11339  prodrbdclem  11352  prodmodclem2  11358  prodmodc  11359  neipsm  12337  dedekindeulemub  12779  dedekindeulemloc  12780  dedekindeulemlub  12781  suplociccex  12786  dedekindicclemub  12788  dedekindicclemloc  12789  dedekindicclemlub  12790  limcimo  12817  nninfalllemn  13263
 Copyright terms: Public domain W3C validator