Theorem rexeqbi1dv 3332

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ∃wrex 3068

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-rex 3069

This theorem is referenced by:  rexeqOLD  3334  friOLD  5636  frsn  5762  isofrlem  7339  f1oweALT  7961  frxp  8114  frxp2  8132  1sdomOLD  9251  oieq2  9510  zfregcl  9591  frmin  9746  hashge2el2difr  14446  cat1  18051  ishaus  23046  isreg  23056  isnrm  23059  lebnumlem3  24709  1vwmgr  29796  3vfriswmgr  29798  isgrpo  30017  pjhth  30913  bnj1154  34308  satfvsuc  34650  satf0suc  34665  sat1el2xp  34668  fmlasuc0  34673  isexid2  37026  ismndo2  37045  rngomndo  37106  stoweidlem28  45042  prprval  46480