Theorem rexeqbi1dv 3337

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 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		raleqbi1dv.1	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))
3	1, 2	rexeqbidvv 3335	1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∃wrex 3092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-rex 3093

This theorem is used by:  frsn  5754  isofrlem  7349  f1oweALT  7978  frxp  8131  frxp2  8149  oieq2  9485  zfregcl  9566  zfregclOLD  9567  frmin  9731  hashge2el2difr  14538  cat1  18179  ishaus  23516  isreg  23526  isnrm  23529  lebnumlem3  25159  1vwmgr  30664  3vfriswmgr  30666  isgrpo  30886  pjhth  31782  bnj1154  35418  satfvsuc  35873  satf0suc  35888  sat1el2xp  35891  fmlasuc0  35896  isexid2  38546  ismndo2  38565  rngomndo  38626  relpfrlem  45702  stoweidlem28  46782  prprval  48303