Theorem rexeq 3294

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 2730	. . 3 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		anbi1 634	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	alexbii 1835	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4	1, 3	sylbi 217	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
5		df-rex 3063	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3063	. 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 3062

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 2709

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

This theorem is referenced by:  raleq  3295  rexeqi  3297  rexeqdv  3299  reueq1  3384  axrep6g  5237  exss  5418  qseq1  8705  pssnn  9105  indexfi  9272  supeq1  9360  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  13234  xrinfmsslem  13235  xrsupss  13236  xrinfmss  13237  hashge2el2difr  14416  cat1  18033  isdrs  18236  isipodrs  18472  neifval  23055  ishaus  23278  2ndc1stc  23407  1stcrest  23409  lly1stc  23452  isref  23465  islocfin  23473  tx1stc  23606  isust  24160  iscfilu  24243  met1stc  24477  iscfil  25233  noetasuplem4  27716  precsexlemcbv  28214  precsexlem3  28217  ishpg  28843  isgrpo  30584  chne0  31581  rprmdvdsprod  33626  constrsuc  33915  constrcbvlem  33932  pstmfval  34073  dya2iocuni  34460  satfvsuc  35574  satf0suc  35589  sat1el2xp  35592  fmlasuc0  35597  altxpeq1  36186  altxpeq2  36187  elhf2  36388  bj-sngleq  37212  cover2g  37964  indexdom  37982  istotbnd  38017  pmapglb2xN  40145  paddval  40171  elpadd0  40182  diophrex  43129  hbtlem1  43477  hbtlem7  43479  tfsconcatb0  43698  mnuop23d  44619  ismnushort  44654  sprval  47836  sprsymrelfvlem  47847  sprsymrelfv  47851  sprsymrelfo  47854  prprval  47871