Theorem rexeq 3316

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-rex 3088

This theorem is used by:  raleq  3317  rexeqi  3319  rexeqdv  3321  reueq1  3398  axrep6g  5243  exss  5431  qseq1  8761  pssnn  9168  indexfi  9333  supeq1  9421  elhf2  9891  bnd2  9937  dfac2b  10190  cflem  10304  cflecard  10311  cfeq0  10315  cfsuc  10316  cfflb  10318  cofsmo  10328  elwina  10752  eltskg  10816  rankcf  10843  elnp  11053  elnpi  11054  genpv  11065  xrsupsslem  13418  xrinfmsslem  13419  xrsupss  13420  xrinfmss  13421  hashge2el2difr  14606  cat1  18252  isdrs  18455  isipodrs  18691  neifval  23397  ishaus  23620  2ndc1stc  23749  1stcrest  23751  lly1stc  23795  isref  23808  islocfin  23816  tx1stc  23949  isust  24503  iscfilu  24586  met1stc  24820  iscfil  25566  noetasuplem4  28075  precsexlemcbv  28574  precsexlem3  28577  ishpg  29219  isgrpo  31081  chne0  32078  rprmdvdsprod  34048  constrsuc  34352  constrcbvlem  34369  pstmfval  34510  dya2iocuni  34898  satfvsuc  36095  satf0suc  36110  sat1el2xp  36113  fmlasuc0  36118  altxpeq1  36708  altxpeq2  36709  bj-sngleq  37850  varprop  38610  negprop  38611  impprop  38612  dfprop2  38614  cover2g  38618  indexdom  38636  istotbnd  38671  pmapglb2xN  40797  paddval  40823  elpadd0  40834  diophrex  43739  hbtlem1  44083  hbtlem7  44085  tfsconcatb0  44304  mnuop23d  45209  ismnushort  45244  sprval  48505  sprsymrelfvlem  48516  sprsymrelfv  48520  sprsymrelfo  48523  prprval  48540