Theorem rexeq 3315

Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2174, ax-11 2190, and ax-12 2211. (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 2754	. . 3 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		anbi1 642	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	alexbii 1852	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4	1, 3	sylbi 219	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
5		df-rex 3086	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3086	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
7	4, 5, 6	3bitr4g 316	1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1557   = wceq 1559  ∃wex 1798   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-rex 3086

This theorem is referenced by:  raleq  3316  rexeqi  3318  rexeqdv  3320  reueq1  3398  axrep6g  5239  exss  5429  qseq1  8733  pssnn  9133  indexfi  9300  supeq1  9388  bnd2  9848  dfac2b  10084  cflem  10198  cflemOLD  10199  cflecard  10206  cfeq0  10210  cfsuc  10211  cfflb  10213  cofsmo  10223  elwina  10641  eltskg  10705  rankcf  10732  elnp  10942  elnpi  10943  genpv  10954  xrsupsslem  13307  xrinfmsslem  13308  xrsupss  13309  xrinfmss  13310  hashge2el2difr  14491  cat1  18113  isdrs  18316  isipodrs  18552  neifval  23139  ishaus  23362  2ndc1stc  23491  1stcrest  23493  lly1stc  23536  isref  23549  islocfin  23557  tx1stc  23690  isust  24244  iscfilu  24327  met1stc  24561  iscfil  25307  noetasuplem4  27777  precsexlemcbv  28276  precsexlem3  28279  ishpg  28905  isgrpo  30646  chne0  31643  rprmdvdsprod  33691  constrsuc  33996  constrcbvlem  34013  pstmfval  34154  dya2iocuni  34541  satfvsuc  35675  satf0suc  35690  sat1el2xp  35693  fmlasuc0  35698  altxpeq1  36287  altxpeq2  36288  elhf2  36489  bj-sngleq  37416  cover2g  38179  indexdom  38197  istotbnd  38232  pmapglb2xN  40360  paddval  40386  elpadd0  40397  diophrex  43320  hbtlem1  43664  hbtlem7  43666  tfsconcatb0  43885  mnuop23d  44806  ismnushort  44841  sprval  48049  sprsymrelfvlem  48060  sprsymrelfv  48064  sprsymrelfo  48067  prprval  48084