Theorem rexeq 3317

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 2215. (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 2755	. . 3 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		anbi1 645	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	alexbii 1866	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4	1, 3	sylbi 220	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
5		df-rex 3089	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3089	. 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 3088

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 2734

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

This theorem is used by:  raleq  3318  rexeqi  3320  rexeqdv  3322  reueq1  3399  axrep6g  5249  exss  5442  qseq1  8760  pssnn  9167  indexfi  9331  supeq1  9419  bnd2  9899  dfac2b  10137  cflem  10251  cflecard  10258  cfeq0  10262  cfsuc  10263  cfflb  10265  cofsmo  10275  elwina  10699  eltskg  10763  rankcf  10790  elnp  11000  elnpi  11001  genpv  11012  xrsupsslem  13363  xrinfmsslem  13364  xrsupss  13365  xrinfmss  13366  hashge2el2difr  14550  cat1  18192  isdrs  18395  isipodrs  18631  neifval  23330  ishaus  23553  2ndc1stc  23682  1stcrest  23684  lly1stc  23728  isref  23741  islocfin  23749  tx1stc  23882  isust  24436  iscfilu  24519  met1stc  24753  iscfil  25499  noetasuplem4  27980  precsexlemcbv  28479  precsexlem3  28482  ishpg  29124  isgrpo  30986  chne0  31983  rprmdvdsprod  33952  constrsuc  34256  constrcbvlem  34273  pstmfval  34414  dya2iocuni  34802  satfvsuc  35948  satf0suc  35963  sat1el2xp  35966  fmlasuc0  35971  altxpeq1  36561  altxpeq2  36562  elhf2  36763  bj-sngleq  37719  cover2g  38474  indexdom  38492  istotbnd  38527  pmapglb2xN  40653  paddval  40679  elpadd0  40690  diophrex  43628  hbtlem1  43972  hbtlem7  43974  tfsconcatb0  44193  mnuop23d  45098  ismnushort  45133  sprval  48387  sprsymrelfvlem  48398  sprsymrelfv  48402  sprsymrelfo  48405  prprval  48422