Theorem rexeq 3319

Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2178, ax-11 2194, and ax-12 2215. (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 2758	. . 3 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		anbi1 644	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	alexbii 1856	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4	1, 3	sylbi 220	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
5		df-rex 3090	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3090	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
7	4, 5, 6	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1561   = wceq 1563  ∃wex 1802   ∈ wcel 2145  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-rex 3090

This theorem is referenced by:  raleq  3320  rexeqi  3322  rexeqdv  3324  reueq1  3402  axrep6g  5245  exss  5435  qseq1  8742  pssnn  9141  indexfi  9305  supeq1  9393  bnd2  9867  dfac2b  10102  cflem  10216  cflemOLD  10217  cflecard  10224  cfeq0  10228  cfsuc  10229  cfflb  10231  cofsmo  10241  elwina  10659  eltskg  10723  rankcf  10750  elnp  10960  elnpi  10961  genpv  10972  xrsupsslem  13324  xrinfmsslem  13325  xrsupss  13326  xrinfmss  13327  hashge2el2difr  14508  cat1  18144  isdrs  18347  isipodrs  18583  neifval  23217  ishaus  23440  2ndc1stc  23569  1stcrest  23571  lly1stc  23614  isref  23627  islocfin  23635  tx1stc  23768  isust  24322  iscfilu  24405  met1stc  24639  iscfil  25385  noetasuplem4  27858  precsexlemcbv  28357  precsexlem3  28360  ishpg  28990  isgrpo  30758  chne0  31755  rprmdvdsprod  33741  constrsuc  34045  constrcbvlem  34062  pstmfval  34203  dya2iocuni  34590  satfvsuc  35724  satf0suc  35739  sat1el2xp  35742  fmlasuc0  35747  altxpeq1  36336  altxpeq2  36337  elhf2  36538  bj-sngleq  37464  cover2g  38227  indexdom  38245  istotbnd  38280  pmapglb2xN  40408  paddval  40434  elpadd0  40445  diophrex  43368  hbtlem1  43712  hbtlem7  43714  tfsconcatb0  43933  mnuop23d  44840  ismnushort  44875  sprval  48083  sprsymrelfvlem  48094  sprsymrelfv  48098  sprsymrelfo  48101  prprval  48118