Theorem rexeq 3315

Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2177, ax-11 2193, and ax-12 2212. (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 2753	. . 3 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		anbi1 645	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	alexbii 1865	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4	1, 3	sylbi 220	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
5		df-rex 3087	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3087	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
7	4, 5, 6	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2144  ∃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:  raleq  3316  rexeqi  3318  rexeqdv  3320  reueq1  3397  axrep6g  5242  exss  5430  qseq1  8780  pssnn  9187  indexfi  9352  supeq1  9440  elhf2  9913  bnd2  9959  dfac2b  10212  cflem  10326  cflecard  10333  cfeq0  10337  cfsuc  10338  cfflb  10340  cofsmo  10350  elwina  10774  eltskg  10838  rankcf  10865  elnp  11075  elnpi  11076  genpv  11087  xrsupsslem  13440  xrinfmsslem  13441  xrsupss  13442  xrinfmss  13443  hashge2el2difr  14629  cat1  18277  isdrs  18480  isipodrs  18716  neifval  23422  ishaus  23645  2ndc1stc  23774  1stcrest  23776  lly1stc  23820  isref  23833  islocfin  23841  tx1stc  23974  isust  24528  iscfilu  24611  met1stc  24845  iscfil  25591  noetasuplem4  28098  precsexlemcbv  28597  precsexlem3  28600  ishpg  29242  isgrpo  31104  chne0  32101  rprmdvdsprod  34112  constrsuc  34416  constrcbvlem  34433  pstmfval  34574  dya2iocuni  34961  satfvsuc  36212  satf0suc  36227  sat1el2xp  36230  fmlasuc0  36235  altxpeq1  36830  altxpeq2  36831  bj-sngleq  37972  varprop  38735  negprop  38736  impprop  38737  dfprop2  38739  cover2g  38743  indexdom  38761  istotbnd  38796  pmapglb2xN  40922  paddval  40948  elpadd0  40959  diophrex  43879  hbtlem1  44218  hbtlem7  44220  tfsconcatb0  44439  mnuop23d  45343  ismnushort  45378  sprval  48654  sprsymrelfvlem  48665  sprsymrelfv  48669  sprsymrelfo  48672  prprval  48689