Theorem rexeqbi1dv 3305

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  rexeqOLD  3307  frsn  5702  isofrlem  7274  f1oweALT  7904  frxp  8056  frxp2  8074  oieq2  9399  zfregcl  9480  zfregclOLD  9481  frmin  9642  hashge2el2difr  14388  cat1  18004  ishaus  23237  isreg  23247  isnrm  23250  lebnumlem3  24889  1vwmgr  30256  3vfriswmgr  30258  isgrpo  30477  pjhth  31373  bnj1154  35011  satfvsuc  35405  satf0suc  35420  sat1el2xp  35423  fmlasuc0  35428  isexid2  37894  ismndo2  37913  rngomndo  37974  relpfrlem  45045  stoweidlem28  46125  prprval  47613