Theorem rexeq 3330

Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2141, 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 2733	. . 3 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		anbi1 632	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	alexbii 1831	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4	1, 3	sylbi 217	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
5		df-rex 3077	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3077	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1535   = wceq 1537  ∃wex 1777   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-rex 3077

This theorem is referenced by:  raleq  3331  rexeqi  3333  rexeqdv  3335  reueq1  3426  axrep6g  5311  exss  5483  qseq1  8819  pssnn  9234  1sdomOLD  9312  indexfi  9430  supeq1  9514  bnd2  9962  dfac2b  10200  cflem  10314  cflemOLD  10315  cflecard  10322  cfeq0  10325  cfsuc  10326  cfflb  10328  cofsmo  10338  elwina  10755  eltskg  10819  rankcf  10846  elnp  11056  elnpi  11057  genpv  11068  xrsupsslem  13369  xrinfmsslem  13370  xrsupss  13371  xrinfmss  13372  hashge2el2difr  14530  cat1  18164  isdrs  18371  isipodrs  18607  neifval  23128  ishaus  23351  2ndc1stc  23480  1stcrest  23482  lly1stc  23525  isref  23538  islocfin  23546  tx1stc  23679  isust  24233  iscfilu  24318  met1stc  24555  iscfil  25318  noetasuplem4  27799  precsexlemcbv  28248  precsexlem3  28251  ishpg  28785  isgrpo  30529  chne0  31526  rprmdvdsprod  33527  constrsuc  33728  pstmfval  33842  dya2iocuni  34248  satfvsuc  35329  satf0suc  35344  sat1el2xp  35347  fmlasuc0  35352  altxpeq1  35937  altxpeq2  35938  elhf2  36139  bj-sngleq  36933  cover2g  37676  indexdom  37694  istotbnd  37729  pmapglb2xN  39729  paddval  39755  elpadd0  39766  diophrex  42731  hbtlem1  43080  hbtlem7  43082  tfsconcatb0  43306  mnuop23d  44235  ismnushort  44270  sprval  47353  sprsymrelfvlem  47364  sprsymrelfv  47368  sprsymrelfo  47371  prprval  47388