Theorem rexeqbi1dv 3340

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

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		raleqbi1dv.1	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))
3	1, 2	rexeqbidvv 3338	1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-rex 3096

This theorem is referenced by:  frsn  5747  isofrlem  7336  f1oweALT  7965  frxp  8118  frxp2  8136  oieq2  9471  zfregcl  9552  zfregclOLD  9553  frmin  9717  hashge2el2difr  14514  cat1  18150  ishaus  23444  isreg  23454  isnrm  23457  lebnumlem3  25087  1vwmgr  30564  3vfriswmgr  30566  isgrpo  30786  pjhth  31682  bnj1154  35328  satfvsuc  35748  satf0suc  35763  sat1el2xp  35766  fmlasuc0  35771  isexid2  38389  ismndo2  38408  rngomndo  38469  relpfrlem  45549  stoweidlem28  46629  prprval  48147