Theorem rexeqbi1dv 3305

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-rex 3057

This theorem is referenced by:  rexeqOLD  3307  frsn  5699  isofrlem  7269  f1oweALT  7899  frxp  8051  frxp2  8069  oieq2  9394  zfregcl  9475  zfregclOLD  9476  frmin  9637  hashge2el2difr  14383  cat1  17999  ishaus  23232  isreg  23242  isnrm  23245  lebnumlem3  24884  1vwmgr  30248  3vfriswmgr  30250  isgrpo  30469  pjhth  31365  bnj1154  35003  satfvsuc  35397  satf0suc  35412  sat1el2xp  35415  fmlasuc0  35420  isexid2  37895  ismndo2  37914  rngomndo  37975  relpfrlem  44986  stoweidlem28  46066  prprval  47545