Theorem rexeq 3288

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2111  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-rex 3057

This theorem is referenced by:  raleq  3289  rexeqi  3291  rexeqdv  3293  reueq1  3378  axrep6g  5228  exss  5403  qseq1  8681  pssnn  9078  indexfi  9244  supeq1  9329  bnd2  9786  dfac2b  10022  cflem  10136  cflemOLD  10137  cflecard  10144  cfeq0  10147  cfsuc  10148  cfflb  10150  cofsmo  10160  elwina  10577  eltskg  10641  rankcf  10668  elnp  10878  elnpi  10879  genpv  10890  xrsupsslem  13206  xrinfmsslem  13207  xrsupss  13208  xrinfmss  13209  hashge2el2difr  14388  cat1  18004  isdrs  18207  isipodrs  18443  neifval  23015  ishaus  23238  2ndc1stc  23367  1stcrest  23369  lly1stc  23412  isref  23425  islocfin  23433  tx1stc  23566  isust  24120  iscfilu  24203  met1stc  24437  iscfil  25193  noetasuplem4  27676  precsexlemcbv  28145  precsexlem3  28148  ishpg  28738  isgrpo  30475  chne0  31472  rprmdvdsprod  33497  constrsuc  33749  constrcbvlem  33766  pstmfval  33907  dya2iocuni  34294  satfvsuc  35403  satf0suc  35418  sat1el2xp  35421  fmlasuc0  35426  altxpeq1  36013  altxpeq2  36014  elhf2  36215  bj-sngleq  37007  cover2g  37762  indexdom  37780  istotbnd  37815  pmapglb2xN  39817  paddval  39843  elpadd0  39854  diophrex  42814  hbtlem1  43162  hbtlem7  43164  tfsconcatb0  43383  mnuop23d  44305  ismnushort  44340  sprval  47516  sprsymrelfvlem  47527  sprsymrelfv  47531  sprsymrelfo  47534  prprval  47551