Theorem rexeqbi1dv 3334

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 3332	1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-rex 3090

This theorem is referenced by:  frsn  5749  isofrlem  7338  f1oweALT  7965  frxp  8118  frxp2  8136  oieq2  9471  zfregcl  9552  zfregclOLD  9553  frmin  9717  hashge2el2difr  14514  cat1  18149  ishaus  23479  isreg  23489  isnrm  23492  lebnumlem3  25122  1vwmgr  30627  3vfriswmgr  30629  isgrpo  30849  pjhth  31745  bnj1154  35387  satfvsuc  35853  satf0suc  35868  sat1el2xp  35871  fmlasuc0  35876  isexid2  38506  ismndo2  38525  rngomndo  38586  relpfrlem  45662  stoweidlem28  46742  prprval  48263