Theorem rexeqbi1dv 3331

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

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

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 2155  ax-ext 2733

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

This theorem is used by:  frsn  5739  isofrlem  7346  f1oweALT  7982  frxp  8136  frxp2  8154  oieq2  9500  zfregcl  9581  zfregclOLD  9582  frmin  9746  hashge2el2difr  14619  cat1  18265  ishaus  23633  isreg  23643  isnrm  23646  lebnumlem3  25277  1vwmgr  30870  3vfriswmgr  30872  isgrpo  31092  pjhth  31988  bnj1154  35622  satfvsuc  36105  satf0suc  36120  sat1el2xp  36123  fmlasuc0  36128  varprop  38622  negprop  38623  impprop  38624  dfprop2  38626  isexid2  38769  ismndo2  38788  rngomndo  38849  relpfrlem  45921  stoweidlem28  47007  prprval  48565