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

Theorem eleq2w 2822
Description: Weaker version of eleq2 2827 (but more general than elequ2 2121) not depending on ax-ext 2709 nor df-cleq 2730. (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 2121 . . . 4 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
21anbi2d 629 . . 3 (𝑥 = 𝑦 → ((𝑧 = 𝐴𝑧𝑥) ↔ (𝑧 = 𝐴𝑧𝑦)))
32exbidv 1924 . 2 (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴𝑧𝑥) ↔ ∃𝑧(𝑧 = 𝐴𝑧𝑦)))
4 dfclel 2817 . 2 (𝐴𝑥 ↔ ∃𝑧(𝑧 = 𝐴𝑧𝑥))
5 dfclel 2817 . 2 (𝐴𝑦 ↔ ∃𝑧(𝑧 = 𝐴𝑧𝑦))
63, 4, 53bitr4g 314 1 (𝑥 = 𝑦 → (𝐴𝑥𝐴𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1539  wex 1782  wcel 2106
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-clel 2816
This theorem is referenced by:  clelsb2  2867  eluniab  4854  elintab  4890  cantnflem1c  9445  tcrank  9642  isf32lem2  10110  sadcp1  16162  subgacs  18789  nsgacs  18790  sdrgacs  20069  lssacs  20229  elcls3  22234  conncompconn  22583  1stcfb  22596  dfac14lem  22768  r0cld  22889  uffix  23072  flftg  23147  tgpconncompeqg  23263  wilth  26220  tghilberti2  26999  umgr2edgneu  27581  uspgredg2v  27591  usgredgleordALT  27601  nbusgrf1o  27738  vtxdushgrfvedglem  27856  ddemeas  32204  cvmcov  33225  cvmseu  33238  sat1el2xp  33341  hilbert1.2  34457  fneint  34537  elintabg  41182  mnuprdlem1  41890  mnuprdlem2  41891  mnuprdlem4  41893  elunif  42559  fnchoice  42572  lmbr3  43288
  Copyright terms: Public domain W3C validator