Theorem rexeqbi1dv 3309

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  rexeqOLD  3311  frsn  5712  isofrlem  7286  f1oweALT  7916  frxp  8068  frxp2  8086  oieq2  9418  zfregcl  9499  zfregclOLD  9500  frmin  9661  hashge2el2difr  14404  cat1  18021  ishaus  23266  isreg  23276  isnrm  23279  lebnumlem3  24918  1vwmgr  30351  3vfriswmgr  30353  isgrpo  30572  pjhth  31468  bnj1154  35155  satfvsuc  35555  satf0suc  35570  sat1el2xp  35573  fmlasuc0  35578  isexid2  38056  ismndo2  38075  rngomndo  38136  relpfrlem  45194  stoweidlem28  46272  prprval  47760