Theorem rexeqbi1dv 3334

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 23	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		raleqbi1dv.1	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜓))
3	1, 2	rexeqbidvv 3332	1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-rex 3091

This theorem is used by:  frsn  5747  isofrlem  7379  f1oweALT  8018  frxp  8175  frxp2  8198  oieq2  9544  zfregcl  9625  zfregclOLD  9626  frmin  9790  hashge2el2difr  14667  cat1  18322  ishaus  23695  isreg  23705  isnrm  23708  lebnumlem3  25339  1vwmgr  30934  3vfriswmgr  30936  isgrpo  31156  pjhth  32052  bnj1154  35740  satfvsuc  36334  satf0suc  36349  sat1el2xp  36352  fmlasuc0  36357  mirimanofffr  36670  varprop  38910  negprop  38911  impprop  38912  dfprop2  38914  isexid2  39055  ismndo2  39074  rngomndo  39135  relpfrlem  46207  stoweidlem28  47311  prprval  48869