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

Theorem rexeqbi1dv 3323
 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 3321 1 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1539  ∃wrex 3072 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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730 This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-cleq 2751  df-clel 2831  df-rex 3077 This theorem is referenced by:  rexeq  3325  fri  5484  frsn  5606  isofrlem  7085  f1oweALT  7675  frxp  7823  1sdom  8740  oieq2  9000  zfregcl  9081  hashge2el2difr  13881  ishaus  22012  isreg  22022  isnrm  22025  lebnumlem3  23654  1vwmgr  28150  3vfriswmgr  28152  isgrpo  28369  pjhth  29265  bnj1154  32489  satfvsuc  32829  satf0suc  32844  sat1el2xp  32847  fmlasuc0  32852  frmin  33324  frxp2  33336  frxp3  33342  isexid2  35563  ismndo2  35582  rngomndo  35643  stoweidlem28  43026  prprval  44389
 Copyright terms: Public domain W3C validator