Theorem rexeqbi1dv 3318

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-rex 3061

This theorem is referenced by:  rexeqOLD  3320  friOLD  5612  frsn  5742  isofrlem  7333  f1oweALT  7971  frxp  8125  frxp2  8143  1sdomOLD  9257  oieq2  9527  zfregcl  9608  frmin  9763  hashge2el2difr  14499  cat1  18110  ishaus  23260  isreg  23270  isnrm  23273  lebnumlem3  24913  1vwmgr  30257  3vfriswmgr  30259  isgrpo  30478  pjhth  31374  bnj1154  35030  satfvsuc  35383  satf0suc  35398  sat1el2xp  35401  fmlasuc0  35406  isexid2  37879  ismndo2  37898  rngomndo  37959  relpfrlem  44978  stoweidlem28  46057  prprval  47528