Theorem rexeqbi1dv 3330

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-rex 3087

This theorem is used by:  frsn  5740  isofrlem  7352  f1oweALT  7988  frxp  8144  frxp2  8167  oieq2  9514  zfregcl  9595  zfregclOLD  9596  frmin  9760  hashge2el2difr  14633  cat1  18281  ishaus  23649  isreg  23659  isnrm  23662  lebnumlem3  25293  1vwmgr  30886  3vfriswmgr  30888  isgrpo  31108  pjhth  32004  bnj1154  35679  satfvsuc  36216  satf0suc  36231  sat1el2xp  36234  fmlasuc0  36239  varprop  38751  negprop  38752  impprop  38753  dfprop2  38755  isexid2  38898  ismndo2  38917  rngomndo  38978  relpfrlem  46051  stoweidlem28  47146  prprval  48704