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

Theorem eleq2w 2818
Description: Weaker version of eleq2 2823 (but more general than elequ2 2122) not depending on ax-ext 2704 nor df-cleq 2725. (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 2122 . . . 4 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
21anbi2d 630 . . 3 (𝑥 = 𝑦 → ((𝑧 = 𝐴𝑧𝑥) ↔ (𝑧 = 𝐴𝑧𝑦)))
32exbidv 1925 . 2 (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴𝑧𝑥) ↔ ∃𝑧(𝑧 = 𝐴𝑧𝑦)))
4 dfclel 2812 . 2 (𝐴𝑥 ↔ ∃𝑧(𝑧 = 𝐴𝑧𝑥))
5 dfclel 2812 . 2 (𝐴𝑦 ↔ ∃𝑧(𝑧 = 𝐴𝑧𝑦))
63, 4, 53bitr4g 314 1 (𝑥 = 𝑦 → (𝐴𝑥𝐴𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wex 1782  wcel 2107
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-clel 2811
This theorem is referenced by:  clelsb2  2862  eluniab  4884  elintabg  4922  elintabOLD  4924  cantnflem1c  9631  tcrank  9828  isf32lem2  10298  sadcp1  16343  subgacs  18971  nsgacs  18972  sdrgacs  20311  lssacs  20472  elcls3  22457  conncompconn  22806  1stcfb  22819  dfac14lem  22991  r0cld  23112  uffix  23295  flftg  23370  tgpconncompeqg  23486  wilth  26443  tghilberti2  27629  umgr2edgneu  28211  uspgredg2v  28221  usgredgleordALT  28231  nbusgrf1o  28368  vtxdushgrfvedglem  28486  ddemeas  32899  cvmcov  33921  cvmseu  33934  sat1el2xp  34037  hilbert1.2  34793  fneint  34873  mnuprdlem1  42644  mnuprdlem2  42645  mnuprdlem4  42647  elunif  43313  fnchoice  43326  lmbr3  44078
  Copyright terms: Public domain W3C validator