MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eleq2w Structured version   Visualization version   GIF version

Theorem eleq2w 2834
Description: Weaker version of eleq2 2839 (but more general than elequ2 2159) not depending on ax-ext 2751 nor df-cleq 2764. (Contributed by BJ, 29-Sep-2019.)
Assertion
Ref Expression
eleq2w (𝑥 = 𝑦 → (𝐴𝑥𝐴𝑦))

Proof of Theorem eleq2w
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 elequ2 2159 . . . 4 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
21anbi2d 614 . . 3 (𝑥 = 𝑦 → ((𝑧 = 𝐴𝑧𝑥) ↔ (𝑧 = 𝐴𝑧𝑦)))
32exbidv 2002 . 2 (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴𝑧𝑥) ↔ ∃𝑧(𝑧 = 𝐴𝑧𝑦)))
4 df-clel 2767 . 2 (𝐴𝑥 ↔ ∃𝑧(𝑧 = 𝐴𝑧𝑥))
5 df-clel 2767 . 2 (𝐴𝑦 ↔ ∃𝑧(𝑧 = 𝐴𝑧𝑦))
63, 4, 53bitr4g 303 1 (𝑥 = 𝑦 → (𝐴𝑥𝐴𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wex 1852  wcel 2145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-clel 2767
This theorem is referenced by:  eluniab  4585  elintab  4622  cantnflem1c  8748  tcrank  8911  isf32lem2  9378  sadcp1  15385  subgacs  17837  nsgacs  17838  lssacs  19180  elcls3  21108  conncompconn  21456  1stcfb  21469  dfac14lem  21641  r0cld  21762  uffix  21945  flftg  22020  tgpconncompeqg  22135  wilth  25018  tghilberti2  25754  umgr2edgneu  26328  uspgredg2v  26338  usgredgleordALT  26349  nbusgrf1o  26496  vtxdushgrfvedglem  26620  ddemeas  30639  cvmcov  31583  cvmseu  31596  hilbert1.2  32599  fneint  32680  sdrgacs  38297  elintabg  38406  elunif  39697  fnchoice  39710  lmbr3  40497
  Copyright terms: Public domain W3C validator