Theorem rexeq 3291

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-rex 3062

This theorem is referenced by:  raleq  3292  rexeqi  3294  rexeqdv  3296  reueq1  3374  axrep6g  5225  exss  5415  qseq1  8703  pssnn  9103  indexfi  9270  supeq1  9358  bnd2  9817  dfac2b  10053  cflem  10167  cflemOLD  10168  cflecard  10175  cfeq0  10178  cfsuc  10179  cfflb  10181  cofsmo  10191  elwina  10609  eltskg  10673  rankcf  10700  elnp  10910  elnpi  10911  genpv  10922  xrsupsslem  13259  xrinfmsslem  13260  xrsupss  13261  xrinfmss  13262  hashge2el2difr  14443  cat1  18064  isdrs  18267  isipodrs  18503  neifval  23064  ishaus  23287  2ndc1stc  23416  1stcrest  23418  lly1stc  23461  isref  23474  islocfin  23482  tx1stc  23615  isust  24169  iscfilu  24252  met1stc  24486  iscfil  25232  noetasuplem4  27700  precsexlemcbv  28198  precsexlem3  28201  ishpg  28827  isgrpo  30568  chne0  31565  rprmdvdsprod  33594  constrsuc  33882  constrcbvlem  33899  pstmfval  34040  dya2iocuni  34427  satfvsuc  35543  satf0suc  35558  sat1el2xp  35561  fmlasuc0  35566  altxpeq1  36155  altxpeq2  36156  elhf2  36357  bj-sngleq  37274  cover2g  38037  indexdom  38055  istotbnd  38090  pmapglb2xN  40218  paddval  40244  elpadd0  40255  diophrex  43207  hbtlem1  43551  hbtlem7  43553  tfsconcatb0  43772  mnuop23d  44693  ismnushort  44728  sprval  47939  sprsymrelfvlem  47950  sprsymrelfv  47954  sprsymrelfo  47957  prprval  47974