Theorem rexeqbi1dv 3306

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 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		raleqbi1dv.1	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))
3	1, 2	rexeqbidvv 3303	1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ∃wrex 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-rex 3058

This theorem is referenced by:  rexeqOLD  3308  frsn  5709  isofrlem  7283  f1oweALT  7913  frxp  8065  frxp2  8083  oieq2  9410  zfregcl  9491  zfregclOLD  9492  frmin  9653  hashge2el2difr  14395  cat1  18012  ishaus  23257  isreg  23267  isnrm  23270  lebnumlem3  24909  1vwmgr  30277  3vfriswmgr  30279  isgrpo  30498  pjhth  31394  bnj1154  35083  satfvsuc  35477  satf0suc  35492  sat1el2xp  35495  fmlasuc0  35500  isexid2  37968  ismndo2  37987  rngomndo  38048  relpfrlem  45110  stoweidlem28  46188  prprval  47676