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

Theorem eleq2w 2862
Description: Weaker version of eleq2 2867 (but more general than elequ2 2171) not depending on ax-ext 2777 nor df-cleq 2792. (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 2171 . . . 4 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
21anbi2d 623 . . 3 (𝑥 = 𝑦 → ((𝑧 = 𝐴𝑧𝑥) ↔ (𝑧 = 𝐴𝑧𝑦)))
32exbidv 2017 . 2 (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝐴𝑧𝑥) ↔ ∃𝑧(𝑧 = 𝐴𝑧𝑦)))
4 df-clel 2795 . 2 (𝐴𝑥 ↔ ∃𝑧(𝑧 = 𝐴𝑧𝑥))
5 df-clel 2795 . 2 (𝐴𝑦 ↔ ∃𝑧(𝑧 = 𝐴𝑧𝑦))
63, 4, 53bitr4g 306 1 (𝑥 = 𝑦 → (𝐴𝑥𝐴𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385   = wceq 1653  wex 1875  wcel 2157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166
This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-clel 2795
This theorem is referenced by:  eluniab  4639  elintab  4678  cantnflem1c  8834  tcrank  8997  isf32lem2  9464  sadcp1  15512  subgacs  17942  nsgacs  17943  lssacs  19288  elcls3  21216  conncompconn  21564  1stcfb  21577  dfac14lem  21749  r0cld  21870  uffix  22053  flftg  22128  tgpconncompeqg  22243  wilth  25149  tghilberti2  25889  umgr2edgneu  26447  uspgredg2v  26457  usgredgleordALT  26468  nbusgrf1o  26615  vtxdushgrfvedglem  26739  ddemeas  30815  cvmcov  31762  cvmseu  31775  hilbert1.2  32775  fneint  32855  sdrgacs  38556  elintabg  38663  elunif  39935  fnchoice  39948  lmbr3  40723
  Copyright terms: Public domain W3C validator