Theorem rexeqbi1dv 3339

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ∃wrex 3070

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 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-rex 3071

This theorem is referenced by:  rexeqOLD  3341  friOLD  5643  frsn  5773  isofrlem  7360  f1oweALT  7997  frxp  8151  frxp2  8169  1sdomOLD  9285  oieq2  9553  zfregcl  9634  frmin  9789  hashge2el2difr  14520  cat1  18142  ishaus  23330  isreg  23340  isnrm  23343  lebnumlem3  24995  1vwmgr  30295  3vfriswmgr  30297  isgrpo  30516  pjhth  31412  bnj1154  35013  satfvsuc  35366  satf0suc  35381  sat1el2xp  35384  fmlasuc0  35389  isexid2  37862  ismndo2  37881  rngomndo  37942  relpfrlem  44974  stoweidlem28  46043  prprval  47501