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

Theorem rexeqbi1dv 3119
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 3111 . 2 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑))
2 raleqd.1 . . 3 (𝐴 = 𝐵 → (𝜑𝜓))
32rexbidv 3029 . 2 (𝐴 = 𝐵 → (∃𝑥𝐵 𝜑 ↔ ∃𝑥𝐵 𝜓))
41, 3bitrd 266 1 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wrex 2892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-cleq 2598  df-clel 2601  df-nfc 2735  df-rex 2897
This theorem is referenced by:  fri  4986  frsn  5098  isofrlem  6464  f1oweALT  7016  frxp  7147  1sdom  8021  oieq2  8274  zfregcl  8355  zfregclOLD  8357  ishaus  20874  isreg  20884  isnrm  20887  lebnumlem3  22497  1vwmgra  26292  3vfriswmgra  26294  isgrpo  26497  pjhth  27438  bnj1154  30123  frmin  30785  isexid2  32623  ismndo2  32642  rngomndo  32703  stoweidlem28  38721  1vwmgr  41444  3vfriswmgr  41446
  Copyright terms: Public domain W3C validator