Theorem rexeq 3321

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1537   = wceq 1539  ∃wex 1778   ∈ wcel 2107  ∃wrex 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

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

This theorem is referenced by:  raleq  3322  rexeqi  3324  rexeqdv  3326  reueq1  3416  axrep6g  5289  exss  5467  qseq1  8802  pssnn  9209  1sdomOLD  9286  indexfi  9401  supeq1  9486  bnd2  9934  dfac2b  10172  cflem  10286  cflemOLD  10287  cflecard  10294  cfeq0  10297  cfsuc  10298  cfflb  10300  cofsmo  10310  elwina  10727  eltskg  10791  rankcf  10818  elnp  11028  elnpi  11029  genpv  11040  xrsupsslem  13350  xrinfmsslem  13351  xrsupss  13352  xrinfmss  13353  hashge2el2difr  14521  cat1  18143  isdrs  18348  isipodrs  18583  neifval  23108  ishaus  23331  2ndc1stc  23460  1stcrest  23462  lly1stc  23505  isref  23518  islocfin  23526  tx1stc  23659  isust  24213  iscfilu  24298  met1stc  24535  iscfil  25300  noetasuplem4  27782  precsexlemcbv  28231  precsexlem3  28234  ishpg  28768  isgrpo  30517  chne0  31514  rprmdvdsprod  33563  constrsuc  33780  pstmfval  33896  dya2iocuni  34286  satfvsuc  35367  satf0suc  35382  sat1el2xp  35385  fmlasuc0  35390  altxpeq1  35975  altxpeq2  35976  elhf2  36177  bj-sngleq  36969  cover2g  37724  indexdom  37742  istotbnd  37777  pmapglb2xN  39775  paddval  39801  elpadd0  39812  diophrex  42791  hbtlem1  43140  hbtlem7  43142  tfsconcatb0  43362  mnuop23d  44290  ismnushort  44325  sprval  47471  sprsymrelfvlem  47482  sprsymrelfv  47486  sprsymrelfo  47489  prprval  47506