Theorem rexeq 3292

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

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

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 2123  ax-ext 2708

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

This theorem is referenced by:  raleq  3293  rexeqi  3295  rexeqdv  3297  reueq1  3382  axrep6g  5235  exss  5411  qseq1  8694  pssnn  9093  indexfi  9260  supeq1  9348  bnd2  9805  dfac2b  10041  cflem  10155  cflemOLD  10156  cflecard  10163  cfeq0  10166  cfsuc  10167  cfflb  10169  cofsmo  10179  elwina  10597  eltskg  10661  rankcf  10688  elnp  10898  elnpi  10899  genpv  10910  xrsupsslem  13222  xrinfmsslem  13223  xrsupss  13224  xrinfmss  13225  hashge2el2difr  14404  cat1  18021  isdrs  18224  isipodrs  18460  neifval  23043  ishaus  23266  2ndc1stc  23395  1stcrest  23397  lly1stc  23440  isref  23453  islocfin  23461  tx1stc  23594  isust  24148  iscfilu  24231  met1stc  24465  iscfil  25221  noetasuplem4  27704  precsexlemcbv  28202  precsexlem3  28205  ishpg  28831  isgrpo  30572  chne0  31569  rprmdvdsprod  33615  constrsuc  33895  constrcbvlem  33912  pstmfval  34053  dya2iocuni  34440  satfvsuc  35555  satf0suc  35570  sat1el2xp  35573  fmlasuc0  35578  altxpeq1  36167  altxpeq2  36168  elhf2  36369  bj-sngleq  37168  cover2g  37917  indexdom  37935  istotbnd  37970  pmapglb2xN  40032  paddval  40058  elpadd0  40069  diophrex  43017  hbtlem1  43365  hbtlem7  43367  tfsconcatb0  43586  mnuop23d  44507  ismnushort  44542  sprval  47725  sprsymrelfvlem  47736  sprsymrelfv  47740  sprsymrelfo  47743  prprval  47760