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

Theorem rexeqbi1dv 3410
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, 2rexeqbidv 3408 1 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1530  wrex 3144
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2819  df-clel 2898  df-rex 3149
This theorem is referenced by:  rexeq  3412  fri  5516  frsn  5638  isofrlem  7085  f1oweALT  7664  frxp  7811  1sdom  8710  oieq2  8966  zfregcl  9047  hashge2el2difr  13829  ishaus  21846  isreg  21856  isnrm  21859  lebnumlem3  23482  1vwmgr  27969  3vfriswmgr  27971  isgrpo  28188  pjhth  29084  bnj1154  32155  satfvsuc  32492  satf0suc  32507  sat1el2xp  32510  fmlasuc0  32515  frmin  32968  isexid2  35001  ismndo2  35020  rngomndo  35081  stoweidlem28  42179  prprval  43508
  Copyright terms: Public domain W3C validator