Theorem rexeqbi1dv 3347

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-rex 3077

This theorem is referenced by:  rexeqOLD  3349  friOLD  5658  frsn  5787  isofrlem  7376  f1oweALT  8013  frxp  8167  frxp2  8185  1sdomOLD  9312  oieq2  9582  zfregcl  9663  frmin  9818  hashge2el2difr  14530  cat1  18164  ishaus  23351  isreg  23361  isnrm  23364  lebnumlem3  25014  1vwmgr  30308  3vfriswmgr  30310  isgrpo  30529  pjhth  31425  bnj1154  34975  satfvsuc  35329  satf0suc  35344  sat1el2xp  35347  fmlasuc0  35352  isexid2  37815  ismndo2  37834  rngomndo  37895  stoweidlem28  45949  prprval  47388