Theorem rexeqbi1dv 3341

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ∃wrex 3065

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-ral 3069  df-rex 3070

This theorem is referenced by:  rexeq  3343  friOLD  5550  frsn  5674  isofrlem  7211  f1oweALT  7815  frxp  7967  1sdom  9025  oieq2  9272  zfregcl  9353  frmin  9507  hashge2el2difr  14195  cat1  17812  ishaus  22473  isreg  22483  isnrm  22486  lebnumlem3  24126  1vwmgr  28640  3vfriswmgr  28642  isgrpo  28859  pjhth  29755  bnj1154  32979  satfvsuc  33323  satf0suc  33338  sat1el2xp  33341  fmlasuc0  33346  frxp2  33791  frxp3  33797  isexid2  36013  ismndo2  36032  rngomndo  36093  stoweidlem28  43569  prprval  44966