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

Theorem rexeqbi1dv 3335
Description: Equality deduction for restricted existential quantifier. (Contributed by NM, 18-Mar-1997.) (Proof shortened by Steven Nguyen, 5-May-2023.)
Hypothesis
Ref Expression
raleqbi1dv.1 (𝐴 = 𝐵 → (𝜑𝜓))
Assertion
Ref Expression
rexeqbi1dv (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem rexeqbi1dv
StepHypRef Expression
1 id 22 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
2 raleqbi1dv.1 . 2 (𝐴 = 𝐵 → (𝜑𝜓))
31, 2rexeqbidvv 3332 1 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wrex 3071
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 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-rex 3072
This theorem is referenced by:  rexeqOLD  3337  friOLD  5633  frsn  5758  isofrlem  7324  f1oweALT  7946  frxp  8099  frxp2  8117  1sdomOLD  9237  oieq2  9495  zfregcl  9576  frmin  9731  hashge2el2difr  14429  cat1  18034  ishaus  22795  isreg  22805  isnrm  22808  lebnumlem3  24448  1vwmgr  29496  3vfriswmgr  29498  isgrpo  29715  pjhth  30611  bnj1154  33941  satfvsuc  34283  satf0suc  34298  sat1el2xp  34301  fmlasuc0  34306  isexid2  36629  ismndo2  36648  rngomndo  36709  stoweidlem28  44617  prprval  46055
  Copyright terms: Public domain W3C validator