Theorem rexeq 3319

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2147  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-rex 3091

This theorem is used by:  raleq  3320  rexeqi  3322  rexeqdv  3324  reueq1  3401  axrep6g  5247  exss  5436  qseq1  8808  pssnn  9215  indexfi  9380  supeq1  9467  elhf2  9940  bnd2  9986  dfac2b  10239  cflem  10353  cflecard  10360  cfeq0  10364  cfsuc  10365  cfflb  10367  cofsmo  10377  elwina  10801  eltskg  10865  rankcf  10892  elnp  11102  elnpi  11103  genpv  11114  xrsupsslem  13467  xrinfmsslem  13468  xrsupss  13469  xrinfmss  13470  hashge2el2difr  14656  cat1  18304  isdrs  18507  isipodrs  18743  neifval  23450  ishaus  23673  2ndc1stc  23802  1stcrest  23804  lly1stc  23848  isref  23861  islocfin  23869  tx1stc  24002  isust  24556  iscfilu  24639  met1stc  24873  iscfil  25619  noetasuplem4  28126  precsexlemcbv  28625  precsexlem3  28628  ishpg  29270  isgrpo  31132  chne0  32129  rprmdvdsprod  34150  constrsuc  34453  constrcbvlem  34470  pstmfval  34611  dya2iocuni  34998  satfvsuc  36306  satf0suc  36321  sat1el2xp  36324  fmlasuc0  36329  altxpeq1  36929  altxpeq2  36930  bj-sngleq  38071  varprop  38847  negprop  38848  impprop  38849  dfprop2  38851  cover2g  38855  indexdom  38873  istotbnd  38906  pmapglb2xN  41032  paddval  41058  elpadd0  41069  diophrex  43990  hbtlem1  44328  hbtlem7  44330  tfsconcatb0  44549  mnuop23d  45453  ismnushort  45488  sprval  48776  sprsymrelfvlem  48787  sprsymrelfv  48791  sprsymrelfo  48794  prprval  48811