Theorem rexeq 3289

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

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 2705

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

This theorem is referenced by:  raleq  3290  rexeqi  3292  rexeqdv  3294  reueq1  3379  axrep6g  5232  exss  5408  qseq1  8689  pssnn  9087  indexfi  9253  supeq1  9338  bnd2  9795  dfac2b  10031  cflem  10145  cflemOLD  10146  cflecard  10153  cfeq0  10156  cfsuc  10157  cfflb  10159  cofsmo  10169  elwina  10586  eltskg  10650  rankcf  10677  elnp  10887  elnpi  10888  genpv  10899  xrsupsslem  13210  xrinfmsslem  13211  xrsupss  13212  xrinfmss  13213  hashge2el2difr  14392  cat1  18008  isdrs  18211  isipodrs  18447  neifval  23017  ishaus  23240  2ndc1stc  23369  1stcrest  23371  lly1stc  23414  isref  23427  islocfin  23435  tx1stc  23568  isust  24122  iscfilu  24205  met1stc  24439  iscfil  25195  noetasuplem4  27678  precsexlemcbv  28147  precsexlem3  28150  ishpg  28740  isgrpo  30481  chne0  31478  rprmdvdsprod  33508  constrsuc  33774  constrcbvlem  33791  pstmfval  33932  dya2iocuni  34319  satfvsuc  35428  satf0suc  35443  sat1el2xp  35446  fmlasuc0  35451  altxpeq1  36040  altxpeq2  36041  elhf2  36242  bj-sngleq  37034  cover2g  37779  indexdom  37797  istotbnd  37832  pmapglb2xN  39894  paddval  39920  elpadd0  39931  diophrex  42895  hbtlem1  43243  hbtlem7  43245  tfsconcatb0  43464  mnuop23d  44386  ismnushort  44421  sprval  47606  sprsymrelfvlem  47617  sprsymrelfv  47621  sprsymrelfo  47624  prprval  47641