Theorem rexeqbi1dv 3404

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  ∃wrex 3139

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893  df-rex 3144

This theorem is referenced by:  rexeq  3406  fri  5517  frsn  5639  isofrlem  7093  f1oweALT  7673  frxp  7820  1sdom  8721  oieq2  8977  zfregcl  9058  hashge2el2difr  13840  ishaus  21930  isreg  21940  isnrm  21943  lebnumlem3  23567  1vwmgr  28055  3vfriswmgr  28057  isgrpo  28274  pjhth  29170  bnj1154  32271  satfvsuc  32608  satf0suc  32623  sat1el2xp  32626  fmlasuc0  32631  frmin  33084  isexid2  35148  ismndo2  35167  rngomndo  35228  stoweidlem28  42333  prprval  43696