Theorem rexeq 3292

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-rex 3063

This theorem is referenced by:  raleq  3293  rexeqi  3295  rexeqdv  3297  reueq1  3375  axrep6g  5225  exss  5410  qseq1  8696  pssnn  9096  indexfi  9263  supeq1  9351  bnd2  9808  dfac2b  10044  cflem  10158  cflemOLD  10159  cflecard  10166  cfeq0  10169  cfsuc  10170  cfflb  10172  cofsmo  10182  elwina  10600  eltskg  10664  rankcf  10691  elnp  10901  elnpi  10902  genpv  10913  xrsupsslem  13250  xrinfmsslem  13251  xrsupss  13252  xrinfmss  13253  hashge2el2difr  14434  cat1  18055  isdrs  18258  isipodrs  18494  neifval  23074  ishaus  23297  2ndc1stc  23426  1stcrest  23428  lly1stc  23471  isref  23484  islocfin  23492  tx1stc  23625  isust  24179  iscfilu  24262  met1stc  24496  iscfil  25242  noetasuplem4  27714  precsexlemcbv  28212  precsexlem3  28215  ishpg  28841  isgrpo  30583  chne0  31580  rprmdvdsprod  33609  constrsuc  33898  constrcbvlem  33915  pstmfval  34056  dya2iocuni  34443  satfvsuc  35559  satf0suc  35574  sat1el2xp  35577  fmlasuc0  35582  altxpeq1  36171  altxpeq2  36172  elhf2  36373  bj-sngleq  37290  cover2g  38051  indexdom  38069  istotbnd  38104  pmapglb2xN  40232  paddval  40258  elpadd0  40269  diophrex  43221  hbtlem1  43569  hbtlem7  43571  tfsconcatb0  43790  mnuop23d  44711  ismnushort  44746  sprval  47951  sprsymrelfvlem  47962  sprsymrelfv  47966  sprsymrelfo  47969  prprval  47986