Theorem rexeq 3297

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 2723	. . 3 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		anbi1 633	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	alexbii 1833	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4	1, 3	sylbi 217	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
5		df-rex 3055	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3055	. 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 3054

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 2702

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

This theorem is referenced by:  raleq  3298  rexeqi  3300  rexeqdv  3302  reueq1  3391  axrep6g  5248  exss  5426  qseq1  8733  pssnn  9138  1sdomOLD  9203  indexfi  9318  supeq1  9403  bnd2  9853  dfac2b  10091  cflem  10205  cflemOLD  10206  cflecard  10213  cfeq0  10216  cfsuc  10217  cfflb  10219  cofsmo  10229  elwina  10646  eltskg  10710  rankcf  10737  elnp  10947  elnpi  10948  genpv  10959  xrsupsslem  13274  xrinfmsslem  13275  xrsupss  13276  xrinfmss  13277  hashge2el2difr  14453  cat1  18066  isdrs  18269  isipodrs  18503  neifval  22993  ishaus  23216  2ndc1stc  23345  1stcrest  23347  lly1stc  23390  isref  23403  islocfin  23411  tx1stc  23544  isust  24098  iscfilu  24182  met1stc  24416  iscfil  25172  noetasuplem4  27655  precsexlemcbv  28115  precsexlem3  28118  ishpg  28693  isgrpo  30433  chne0  31430  rprmdvdsprod  33512  constrsuc  33735  constrcbvlem  33752  pstmfval  33893  dya2iocuni  34281  satfvsuc  35355  satf0suc  35370  sat1el2xp  35373  fmlasuc0  35378  altxpeq1  35968  altxpeq2  35969  elhf2  36170  bj-sngleq  36962  cover2g  37717  indexdom  37735  istotbnd  37770  pmapglb2xN  39773  paddval  39799  elpadd0  39810  diophrex  42770  hbtlem1  43119  hbtlem7  43121  tfsconcatb0  43340  mnuop23d  44262  ismnushort  44297  sprval  47484  sprsymrelfvlem  47495  sprsymrelfv  47499  sprsymrelfo  47502  prprval  47519