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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-rex 3062

This theorem is referenced by:  frsn  5719  isofrlem  7295  f1oweALT  7925  frxp  8076  frxp2  8094  oieq2  9428  zfregcl  9509  zfregclOLD  9510  frmin  9673  hashge2el2difr  14443  cat1  18064  ishaus  23287  isreg  23297  isnrm  23300  lebnumlem3  24930  1vwmgr  30346  3vfriswmgr  30348  isgrpo  30568  pjhth  31464  bnj1154  35141  satfvsuc  35543  satf0suc  35558  sat1el2xp  35561  fmlasuc0  35566  isexid2  38176  ismndo2  38195  rngomndo  38256  relpfrlem  45380  stoweidlem28  46456  prprval  47974