Theorem rexeqbi1dv 3323

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1539  ∃wrex 3072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-cleq 2751  df-clel 2831  df-rex 3077

This theorem is referenced by:  rexeq  3325  fri  5484  frsn  5606  isofrlem  7085  f1oweALT  7675  frxp  7823  1sdom  8740  oieq2  9000  zfregcl  9081  hashge2el2difr  13881  ishaus  22012  isreg  22022  isnrm  22025  lebnumlem3  23654  1vwmgr  28150  3vfriswmgr  28152  isgrpo  28369  pjhth  29265  bnj1154  32489  satfvsuc  32829  satf0suc  32844  sat1el2xp  32847  fmlasuc0  32852  frmin  33324  frxp2  33336  frxp3  33342  isexid2  35563  ismndo2  35582  rngomndo  35643  stoweidlem28  43026  prprval  44389