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

Theorem rexeqbi1dv 3287
 Description: Equality deduction for restricted existential quantifier. (Contributed by NM, 18-Mar-1997.)
Hypothesis
Ref Expression
raleqd.1 (𝐴 = 𝐵 → (𝜑𝜓))
Assertion
Ref Expression
rexeqbi1dv (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem rexeqbi1dv
StepHypRef Expression
1 rexeq 3279 . 2 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑))
2 raleqd.1 . . 3 (𝐴 = 𝐵 → (𝜑𝜓))
32rexbidv 3191 . 2 (𝐴 = 𝐵 → (∃𝑥𝐵 𝜑 ↔ ∃𝑥𝐵 𝜓))
41, 3bitrd 268 1 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1632  ∃wrex 3052 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-ext 2741 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-cleq 2754  df-clel 2757  df-nfc 2892  df-rex 3057 This theorem is referenced by:  fri  5229  frsn  5347  isofrlem  6755  f1oweALT  7319  frxp  7457  1sdom  8331  oieq2  8586  zfregcl  8667  ishaus  21349  isreg  21359  isnrm  21362  lebnumlem3  22984  1vwmgr  27452  3vfriswmgr  27454  isgrpo  27682  pjhth  28583  bnj1154  31396  frmin  32070  isexid2  33986  ismndo2  34005  rngomndo  34066  stoweidlem28  40767
 Copyright terms: Public domain W3C validator