Theorem rexeq 3286

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

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 2701

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

This theorem is referenced by:  raleq  3287  rexeqi  3289  rexeqdv  3291  reueq1  3379  axrep6g  5232  exss  5410  qseq1  8691  pssnn  9092  indexfi  9269  supeq1  9354  bnd2  9808  dfac2b  10044  cflem  10158  cflemOLD  10159  cflecard  10166  cfeq0  10169  cfsuc  10170  cfflb  10172  cofsmo  10182  elwina  10599  eltskg  10663  rankcf  10690  elnp  10900  elnpi  10901  genpv  10912  xrsupsslem  13227  xrinfmsslem  13228  xrsupss  13229  xrinfmss  13230  hashge2el2difr  14406  cat1  18022  isdrs  18225  isipodrs  18461  neifval  23002  ishaus  23225  2ndc1stc  23354  1stcrest  23356  lly1stc  23399  isref  23412  islocfin  23420  tx1stc  23553  isust  24107  iscfilu  24191  met1stc  24425  iscfil  25181  noetasuplem4  27664  precsexlemcbv  28131  precsexlem3  28134  ishpg  28722  isgrpo  30459  chne0  31456  rprmdvdsprod  33484  constrsuc  33707  constrcbvlem  33724  pstmfval  33865  dya2iocuni  34253  satfvsuc  35336  satf0suc  35351  sat1el2xp  35354  fmlasuc0  35359  altxpeq1  35949  altxpeq2  35950  elhf2  36151  bj-sngleq  36943  cover2g  37698  indexdom  37716  istotbnd  37751  pmapglb2xN  39754  paddval  39780  elpadd0  39791  diophrex  42751  hbtlem1  43099  hbtlem7  43101  tfsconcatb0  43320  mnuop23d  44242  ismnushort  44277  sprval  47467  sprsymrelfvlem  47478  sprsymrelfv  47482  sprsymrelfo  47485  prprval  47502