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

Theorem eleq2w 2896
Description: Weaker version of eleq2 2901 (but more general than elequ2 2125) not depending on ax-ext 2793 nor df-cleq 2814. (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 2125 . . . 4 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
21anbi2d 630 . . 3 (𝑥 = 𝑦 → ((𝑧 = 𝐴𝑧𝑥) ↔ (𝑧 = 𝐴𝑧𝑦)))
32exbidv 1918 . 2 (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴𝑧𝑥) ↔ ∃𝑧(𝑧 = 𝐴𝑧𝑦)))
4 dfclel 2894 . 2 (𝐴𝑥 ↔ ∃𝑧(𝑧 = 𝐴𝑧𝑥))
5 dfclel 2894 . 2 (𝐴𝑦 ↔ ∃𝑧(𝑧 = 𝐴𝑧𝑦))
63, 4, 53bitr4g 316 1 (𝑥 = 𝑦 → (𝐴𝑥𝐴𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398   = wceq 1533  wex 1776  wcel 2110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-clel 2893
This theorem is referenced by:  eluniab  4843  elintab  4880  cantnflem1c  9144  tcrank  9307  isf32lem2  9770  sadcp1  15798  subgacs  18307  nsgacs  18308  sdrgacs  19574  lssacs  19733  elcls3  21685  conncompconn  22034  1stcfb  22047  dfac14lem  22219  r0cld  22340  uffix  22523  flftg  22598  tgpconncompeqg  22714  wilth  25642  tghilberti2  26418  umgr2edgneu  26990  uspgredg2v  27000  usgredgleordALT  27010  nbusgrf1o  27147  vtxdushgrfvedglem  27265  ddemeas  31490  cvmcov  32505  cvmseu  32518  sat1el2xp  32621  hilbert1.2  33611  fneint  33691  elintabg  39927  mnuprdlem1  40601  mnuprdlem2  40602  mnuprdlem4  40604  elunif  41266  fnchoice  41279  lmbr3  42020
  Copyright terms: Public domain W3C validator