Theorem rexeqbi1dv 3330

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-rex 3086

This theorem is referenced by:  frsn  5731  isofrlem  7319  f1oweALT  7948  frxp  8100  frxp2  8118  oieq2  9455  zfregcl  9536  zfregclOLD  9537  frmin  9701  hashge2el2difr  14488  cat1  18121  ishaus  23370  isreg  23380  isnrm  23383  lebnumlem3  25013  1vwmgr  30435  3vfriswmgr  30437  isgrpo  30657  pjhth  31553  bnj1154  35255  satfvsuc  35672  satf0suc  35687  sat1el2xp  35690  fmlasuc0  35695  isexid2  38315  ismndo2  38334  rngomndo  38395  relpfrlem  45490  stoweidlem28  46563  prprval  48081