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

Theorem eleq2w 2893
Description: Weaker version of eleq2 2898 (but more general than elequ2 2120) not depending on ax-ext 2790 nor df-cleq 2811. (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 2120 . . . 4 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
21anbi2d 628 . . 3 (𝑥 = 𝑦 → ((𝑧 = 𝐴𝑧𝑥) ↔ (𝑧 = 𝐴𝑧𝑦)))
32exbidv 1913 . 2 (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴𝑧𝑥) ↔ ∃𝑧(𝑧 = 𝐴𝑧𝑦)))
4 dfclel 2891 . 2 (𝐴𝑥 ↔ ∃𝑧(𝑧 = 𝐴𝑧𝑥))
5 dfclel 2891 . 2 (𝐴𝑦 ↔ ∃𝑧(𝑧 = 𝐴𝑧𝑦))
63, 4, 53bitr4g 315 1 (𝑥 = 𝑦 → (𝐴𝑥𝐴𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wex 1771  wcel 2105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-clel 2890
This theorem is referenced by:  eluniab  4841  elintab  4878  cantnflem1c  9138  tcrank  9301  isf32lem2  9764  sadcp1  15792  subgacs  18251  nsgacs  18252  sdrgacs  19509  lssacs  19668  elcls3  21619  conncompconn  21968  1stcfb  21981  dfac14lem  22153  r0cld  22274  uffix  22457  flftg  22532  tgpconncompeqg  22647  wilth  25575  tghilberti2  26351  umgr2edgneu  26923  uspgredg2v  26933  usgredgleordALT  26943  nbusgrf1o  27080  vtxdushgrfvedglem  27198  ddemeas  31394  cvmcov  32407  cvmseu  32420  sat1el2xp  32523  hilbert1.2  33513  fneint  33593  elintabg  39812  mnuprdlem1  40485  mnuprdlem2  40486  mnuprdlem4  40488  elunif  41150  fnchoice  41163  lmbr3  41904
  Copyright terms: Public domain W3C validator