Theorem rexeq 3294

Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2152, ax-11 2168, and ax-12 2189. (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 2733	. . 3 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		anbi1 639	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	alexbii 1840	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4	1, 3	sylbi 218	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
5		df-rex 3065	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3065	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
7	4, 5, 6	3bitr4g 315	1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1545   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-rex 3065

This theorem is referenced by:  raleq  3295  rexeqi  3297  rexeqdv  3299  reueq1  3377  axrep6g  5219  exss  5409  qseq1  8700  pssnn  9100  indexfi  9267  supeq1  9355  bnd2  9815  dfac2b  10051  cflem  10165  cflemOLD  10166  cflecard  10173  cfeq0  10176  cfsuc  10177  cfflb  10179  cofsmo  10189  elwina  10607  eltskg  10671  rankcf  10698  elnp  10908  elnpi  10909  genpv  10920  xrsupsslem  13257  xrinfmsslem  13258  xrsupss  13259  xrinfmss  13260  hashge2el2difr  14441  cat1  18062  isdrs  18265  isipodrs  18501  neifval  23089  ishaus  23312  2ndc1stc  23441  1stcrest  23443  lly1stc  23486  isref  23499  islocfin  23507  tx1stc  23640  isust  24194  iscfilu  24277  met1stc  24511  iscfil  25257  noetasuplem4  27725  precsexlemcbv  28223  precsexlem3  28226  ishpg  28852  isgrpo  30593  chne0  31590  rprmdvdsprod  33624  constrsuc  33929  constrcbvlem  33946  pstmfval  34087  dya2iocuni  34474  satfvsuc  35596  satf0suc  35611  sat1el2xp  35614  fmlasuc0  35619  altxpeq1  36208  altxpeq2  36209  elhf2  36410  bj-sngleq  37327  cover2g  38090  indexdom  38108  istotbnd  38143  pmapglb2xN  40271  paddval  40297  elpadd0  40308  diophrex  43231  hbtlem1  43575  hbtlem7  43577  tfsconcatb0  43796  mnuop23d  44717  ismnushort  44752  sprval  47961  sprsymrelfvlem  47972  sprsymrelfv  47976  sprsymrelfo  47979  prprval  47996