Theorem rexeq 3320

Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2136, ax-11 2153, and ax-12 2170. (Revised by Steven Nguyen, 30-Apr-2023.) Shorten other proofs. (Revised by Wolf Lammen, 8-Mar-2025.)

Assertion

Ref	Expression
rexeq	⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rexeq

Step	Hyp	Ref	Expression
1		dfcleq 2724	. . 3 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		anbi1 631	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	alexbii 1834	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4	1, 3	sylbi 216	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
5		df-rex 3070	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3070	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1780   ∈ wcel 2105  ∃wrex 3069

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 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

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

This theorem is referenced by:  raleq  3321  rexeqi  3323  rexeqdv  3325  reueq1  3414  unieqOLD  4920  axrep6g  5293  exss  5463  qseq1  8763  pssnn  9174  1sdomOLD  9255  pssnnOLD  9271  indexfi  9366  supeq1  9446  bnd2  9894  dfac2b  10131  cflem  10247  cflecard  10254  cfeq0  10257  cfsuc  10258  cfflb  10260  cofsmo  10270  elwina  10687  eltskg  10751  rankcf  10778  elnp  10988  elnpi  10989  genpv  11000  xrsupsslem  13293  xrinfmsslem  13294  xrsupss  13295  xrinfmss  13296  hashge2el2difr  14449  cat1  18057  isdrs  18264  isipodrs  18500  neifval  22923  ishaus  23146  2ndc1stc  23275  1stcrest  23277  lly1stc  23320  isref  23333  islocfin  23341  tx1stc  23474  isust  24028  iscfilu  24113  met1stc  24350  iscfil  25113  noetasuplem4  27582  precsexlemcbv  28017  precsexlem3  28020  ishpg  28443  isgrpo  30183  chne0  31180  pstmfval  33340  dya2iocuni  33746  satfvsuc  34816  satf0suc  34831  sat1el2xp  34834  fmlasuc0  34839  altxpeq1  35415  altxpeq2  35416  elhf2  35617  bj-sngleq  36312  cover2g  37048  indexdom  37066  istotbnd  37101  pmapglb2xN  39107  paddval  39133  elpadd0  39144  diophrex  41976  hbtlem1  42328  hbtlem7  42330  tfsconcatb0  42557  mnuop23d  43488  ismnushort  43523  sprval  46606  sprsymrelfvlem  46617  sprsymrelfv  46621  sprsymrelfo  46624  prprval  46641