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

Theorem eleq2w 2825
Description: Weaker version of eleq2 2830 (but more general than elequ2 2123) not depending on ax-ext 2708 nor df-cleq 2729. (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 2123 . . . 4 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
21anbi2d 630 . . 3 (𝑥 = 𝑦 → ((𝑧 = 𝐴𝑧𝑥) ↔ (𝑧 = 𝐴𝑧𝑦)))
32exbidv 1921 . 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 206  wa 395   = wceq 1540  wex 1779  wcel 2108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2816
This theorem is referenced by:  clelsb2  2869  eluniab  4921  elintabg  4957  elintabOLD  4959  cantnflem1c  9727  tcrank  9924  isf32lem2  10394  sadcp1  16492  subgacs  19179  nsgacs  19180  sdrgacs  20802  lssacs  20965  elcls3  23091  conncompconn  23440  1stcfb  23453  dfac14lem  23625  r0cld  23746  uffix  23929  flftg  24004  tgpconncompeqg  24120  wilth  27114  tghilberti2  28646  umgr2edgneu  29231  uspgredg2v  29241  usgredgleordALT  29251  nbusgrf1o  29388  vtxdushgrfvedglem  29507  constrmon  33785  ddemeas  34237  cvmcov  35268  cvmseu  35281  sat1el2xp  35384  hilbert1.2  36156  fneint  36349  mnuprdlem1  44291  mnuprdlem2  44292  mnuprdlem4  44294  elunif  45021  fnchoice  45034  lmbr3  45762
  Copyright terms: Public domain W3C validator