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

Theorem rexeq 3409
 Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2144, ax-11 2160, and ax-12 2176. (Revised by Steven Nguyen, 30-Apr-2023.)
Assertion
Ref Expression
rexeq (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rexeq
StepHypRef Expression
1 biidd 264 . 2 (𝐴 = 𝐵 → (𝜑𝜑))
21rexeqbi1dv 3407 1 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   = wceq 1536  ∃wrex 3142 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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2796 This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2817  df-clel 2896  df-rex 3147 This theorem is referenced by:  rexeqi  3417  rexeqdv  3419  rexeqbi1dvOLD  3421  unieqOLD  4853  exss  5358  qseq1  8346  1sdom  8724  pssnn  8739  indexfi  8835  supeq1  8912  bnd2  9325  dfac2b  9559  cflem  9671  cflecard  9678  cfeq0  9681  cfsuc  9682  cfflb  9684  cofsmo  9694  elwina  10111  eltskg  10175  rankcf  10202  elnp  10412  elnpi  10413  genpv  10424  xrsupsslem  12703  xrinfmsslem  12704  xrsupss  12705  xrinfmss  12706  hashge2el2difr  13842  isdrs  17547  isipodrs  17774  neifval  21710  ishaus  21933  2ndc1stc  22062  1stcrest  22064  lly1stc  22107  isref  22120  islocfin  22128  tx1stc  22261  isust  22815  iscfilu  22900  met1stc  23134  iscfil  23871  ishpg  26548  isgrpo  28277  chne0  29274  pstmfval  31140  dya2iocuni  31545  satfvsuc  32612  satf0suc  32627  sat1el2xp  32630  fmlasuc0  32635  noetalem3  33223  altxpeq1  33438  altxpeq2  33439  elhf2  33640  bj-sngleq  34283  cover2g  34994  indexdom  35013  istotbnd  35051  pmapglb2xN  36912  paddval  36938  elpadd0  36949  diophrex  39378  hbtlem1  39729  hbtlem7  39731  mnuop23d  40608  sprval  43648  sprsymrelfvlem  43659  sprsymrelfv  43663  sprsymrelfo  43666  prprval  43683
 Copyright terms: Public domain W3C validator