Theorem rexeqbi1dv 3332

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ral 3068  df-rex 3069

This theorem is referenced by:  rexeq  3334  friOLD  5541  frsn  5665  isofrlem  7191  f1oweALT  7788  frxp  7938  1sdom  8955  oieq2  9202  zfregcl  9283  frmin  9438  hashge2el2difr  14123  cat1  17728  ishaus  22381  isreg  22391  isnrm  22394  lebnumlem3  24032  1vwmgr  28541  3vfriswmgr  28543  isgrpo  28760  pjhth  29656  bnj1154  32879  satfvsuc  33223  satf0suc  33238  sat1el2xp  33241  fmlasuc0  33246  frxp2  33718  frxp3  33724  isexid2  35940  ismndo2  35959  rngomndo  36020  stoweidlem28  43459  prprval  44854