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

Theorem rexeqbi1dv 3339
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 3336 1 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1540  wrex 3070
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-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-rex 3071
This theorem is referenced by:  rexeqOLD  3341  friOLD  5643  frsn  5773  isofrlem  7360  f1oweALT  7997  frxp  8151  frxp2  8169  1sdomOLD  9285  oieq2  9553  zfregcl  9634  frmin  9789  hashge2el2difr  14520  cat1  18142  ishaus  23330  isreg  23340  isnrm  23343  lebnumlem3  24995  1vwmgr  30295  3vfriswmgr  30297  isgrpo  30516  pjhth  31412  bnj1154  35013  satfvsuc  35366  satf0suc  35381  sat1el2xp  35384  fmlasuc0  35389  isexid2  37862  ismndo2  37881  rngomndo  37942  relpfrlem  44974  stoweidlem28  46043  prprval  47501
  Copyright terms: Public domain W3C validator