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  5633  frsn  5758  isofrlem  7324  f1oweALT  7946  frxp  8099  frxp2  8117  1sdomOLD  9237  oieq2  9495  zfregcl  9576  frmin  9731  hashge2el2difr  14429  cat1  18034  ishaus  22795  isreg  22805  isnrm  22808  lebnumlem3  24448  1vwmgr  29496  3vfriswmgr  29498  isgrpo  29715  pjhth  30611  bnj1154  33941  satfvsuc  34283  satf0suc  34298  sat1el2xp  34301  fmlasuc0  34306  isexid2  36629  ismndo2  36648  rngomndo  36709  stoweidlem28  44617  prprval  46055