Theorem rexeqbi1dv 3336

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

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

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 2737

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

This theorem is used by:  frsn  5751  isofrlem  7347  f1oweALT  7975  frxp  8128  frxp2  8146  oieq2  9482  zfregcl  9563  zfregclOLD  9564  frmin  9728  hashge2el2difr  14536  cat1  18176  ishaus  23529  isreg  23539  isnrm  23542  lebnumlem3  25173  1vwmgr  30698  3vfriswmgr  30700  isgrpo  30920  pjhth  31816  bnj1154  35452  satfvsuc  35890  satf0suc  35905  sat1el2xp  35908  fmlasuc0  35913  isexid2  38564  ismndo2  38583  rngomndo  38644  relpfrlem  45720  stoweidlem28  46800  prprval  48321