Theorem rexeqbi1dv 3307

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

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

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 2709

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

This theorem is referenced by:  frsn  5712  isofrlem  7288  f1oweALT  7918  frxp  8069  frxp2  8087  oieq2  9421  zfregcl  9502  zfregclOLD  9503  frmin  9664  hashge2el2difr  14434  cat1  18055  ishaus  23297  isreg  23307  isnrm  23310  lebnumlem3  24940  1vwmgr  30361  3vfriswmgr  30363  isgrpo  30583  pjhth  31479  bnj1154  35157  satfvsuc  35559  satf0suc  35574  sat1el2xp  35577  fmlasuc0  35582  isexid2  38190  ismndo2  38209  rngomndo  38270  relpfrlem  45398  stoweidlem28  46474  prprval  47986