Theorem rexeq 3295

Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2142, ax-11 2158, and ax-12 2178. (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 2722	. . 3 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		anbi1 633	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	alexbii 1833	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4	1, 3	sylbi 217	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
5		df-rex 3054	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3054	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-rex 3054

This theorem is referenced by:  raleq  3296  rexeqi  3298  rexeqdv  3300  reueq1  3388  axrep6g  5245  exss  5423  qseq1  8730  pssnn  9132  1sdomOLD  9196  indexfi  9311  supeq1  9396  bnd2  9846  dfac2b  10084  cflem  10198  cflemOLD  10199  cflecard  10206  cfeq0  10209  cfsuc  10210  cfflb  10212  cofsmo  10222  elwina  10639  eltskg  10703  rankcf  10730  elnp  10940  elnpi  10941  genpv  10952  xrsupsslem  13267  xrinfmsslem  13268  xrsupss  13269  xrinfmss  13270  hashge2el2difr  14446  cat1  18059  isdrs  18262  isipodrs  18496  neifval  22986  ishaus  23209  2ndc1stc  23338  1stcrest  23340  lly1stc  23383  isref  23396  islocfin  23404  tx1stc  23537  isust  24091  iscfilu  24175  met1stc  24409  iscfil  25165  noetasuplem4  27648  precsexlemcbv  28108  precsexlem3  28111  ishpg  28686  isgrpo  30426  chne0  31423  rprmdvdsprod  33505  constrsuc  33728  constrcbvlem  33745  pstmfval  33886  dya2iocuni  34274  satfvsuc  35348  satf0suc  35363  sat1el2xp  35366  fmlasuc0  35371  altxpeq1  35961  altxpeq2  35962  elhf2  36163  bj-sngleq  36955  cover2g  37710  indexdom  37728  istotbnd  37763  pmapglb2xN  39766  paddval  39792  elpadd0  39803  diophrex  42763  hbtlem1  43112  hbtlem7  43114  tfsconcatb0  43333  mnuop23d  44255  ismnushort  44290  sprval  47480  sprsymrelfvlem  47491  sprsymrelfv  47495  sprsymrelfo  47498  prprval  47515