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 1570  ∃wrex 3086

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

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

This theorem is used by:  frsn  5743  isofrlem  7341  f1oweALT  7969  frxp  8124  frxp2  8142  oieq2  9485  zfregcl  9566  zfregclOLD  9567  frmin  9731  hashge2el2difr  14546  cat1  18186  ishaus  23547  isreg  23557  isnrm  23560  lebnumlem3  25191  1vwmgr  30756  3vfriswmgr  30758  isgrpo  30978  pjhth  31874  bnj1154  35508  satfvsuc  35940  satf0suc  35955  sat1el2xp  35958  fmlasuc0  35963  isexid2  38605  ismndo2  38624  rngomndo  38685  relpfrlem  45776  stoweidlem28  46856  prprval  48414