Theorem rexeq 3319

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1568   = wceq 1570  ∃wex 1809   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-rex 3090

This theorem is referenced by:  raleq  3320  rexeqi  3322  rexeqdv  3324  reueq1  3401  axrep6g  5252  exss  5446  qseq1  8755  pssnn  9154  indexfi  9318  supeq1  9406  bnd2  9880  dfac2b  10115  cflem  10229  cflemOLD  10230  cflecard  10237  cfeq0  10241  cfsuc  10242  cfflb  10244  cofsmo  10254  elwina  10672  eltskg  10736  rankcf  10763  elnp  10973  elnpi  10974  genpv  10985  xrsupsslem  13334  xrinfmsslem  13335  xrsupss  13336  xrinfmss  13337  hashge2el2difr  14520  cat1  18155  isdrs  18358  isipodrs  18594  neifval  23237  ishaus  23460  2ndc1stc  23589  1stcrest  23591  lly1stc  23634  isref  23647  islocfin  23655  tx1stc  23788  isust  24342  iscfilu  24425  met1stc  24659  iscfil  25405  noetasuplem4  27881  precsexlemcbv  28380  precsexlem3  28383  ishpg  29022  isgrpo  30830  chne0  31827  rprmdvdsprod  33805  constrsuc  34109  constrcbvlem  34126  pstmfval  34267  dya2iocuni  34654  satfvsuc  35834  satf0suc  35849  sat1el2xp  35852  fmlasuc0  35857  altxpeq1  36446  altxpeq2  36447  elhf2  36648  bj-sngleq  37584  cover2g  38348  indexdom  38366  istotbnd  38401  pmapglb2xN  40527  paddval  40553  elpadd0  40564  diophrex  43489  hbtlem1  43833  hbtlem7  43835  tfsconcatb0  44054  mnuop23d  44959  ismnushort  44994  sprval  48211  sprsymrelfvlem  48222  sprsymrelfv  48226  sprsymrelfo  48229  prprval  48246