Theorem rexeqbi1dv 3314

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

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

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 2008  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  rexeqOLD  3316  frsn  5729  isofrlem  7318  f1oweALT  7954  frxp  8108  frxp2  8126  1sdomOLD  9203  oieq2  9473  zfregcl  9554  frmin  9709  hashge2el2difr  14453  cat1  18066  ishaus  23216  isreg  23226  isnrm  23229  lebnumlem3  24869  1vwmgr  30212  3vfriswmgr  30214  isgrpo  30433  pjhth  31329  bnj1154  34996  satfvsuc  35355  satf0suc  35370  sat1el2xp  35373  fmlasuc0  35378  isexid2  37856  ismndo2  37875  rngomndo  37936  relpfrlem  44950  stoweidlem28  46033  prprval  47519