Theorem rexeqbi1dv 3335

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  ∃wrex 3071

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 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-rex 3072

This theorem is referenced by:  rexeqOLD  3337  friOLD  5638  frsn  5764  isofrlem  7337  f1oweALT  7959  frxp  8112  frxp2  8130  1sdomOLD  9249  oieq2  9508  zfregcl  9589  frmin  9744  hashge2el2difr  14442  cat1  18047  ishaus  22826  isreg  22836  isnrm  22839  lebnumlem3  24479  1vwmgr  29529  3vfriswmgr  29531  isgrpo  29750  pjhth  30646  bnj1154  34010  satfvsuc  34352  satf0suc  34367  sat1el2xp  34370  fmlasuc0  34375  isexid2  36723  ismndo2  36742  rngomndo  36803  stoweidlem28  44744  prprval  46182