Theorem rexeqbi1dv 3309

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

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

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 2701

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

This theorem is referenced by:  rexeqOLD  3311  frsn  5719  isofrlem  7297  f1oweALT  7930  frxp  8082  frxp2  8100  1sdomOLD  9172  oieq2  9442  zfregcl  9523  frmin  9678  hashge2el2difr  14422  cat1  18035  ishaus  23185  isreg  23195  isnrm  23198  lebnumlem3  24838  1vwmgr  30178  3vfriswmgr  30180  isgrpo  30399  pjhth  31295  bnj1154  34962  satfvsuc  35321  satf0suc  35336  sat1el2xp  35339  fmlasuc0  35344  isexid2  37822  ismndo2  37841  rngomndo  37902  relpfrlem  44916  stoweidlem28  45999  prprval  47488