Theorem rexeq 3322

Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2179, ax-11 2195, 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 2759	. . 3 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		anbi1 645	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	alexbii 1866	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4	1, 3	sylbi 220	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
5		df-rex 3093	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3093	. 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 2146  ∃wrex 3092

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 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

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

This theorem is used by:  raleq  3323  rexeqi  3325  rexeqdv  3327  reueq1  3404  axrep6g  5256  exss  5449  qseq1  8763  pssnn  9163  indexfi  9327  supeq1  9415  bnd2  9895  dfac2b  10133  cflem  10247  cflecard  10254  cfeq0  10258  cfsuc  10259  cfflb  10261  cofsmo  10271  elwina  10689  eltskg  10753  rankcf  10780  elnp  10990  elnpi  10991  genpv  11002  xrsupsslem  13351  xrinfmsslem  13352  xrsupss  13353  xrinfmss  13354  hashge2el2difr  14538  cat1  18179  isdrs  18382  isipodrs  18618  neifval  23293  ishaus  23516  2ndc1stc  23645  1stcrest  23647  lly1stc  23690  isref  23703  islocfin  23711  tx1stc  23844  isust  24398  iscfilu  24481  met1stc  24715  iscfil  25461  noetasuplem4  27937  precsexlemcbv  28436  precsexlem3  28439  ishpg  29078  isgrpo  30886  chne0  31883  rprmdvdsprod  33855  constrsuc  34159  constrcbvlem  34176  pstmfval  34317  dya2iocuni  34705  satfvsuc  35874  satf0suc  35889  sat1el2xp  35892  fmlasuc0  35897  altxpeq1  36486  altxpeq2  36487  elhf2  36688  bj-sngleq  37644  cover2g  38408  indexdom  38426  istotbnd  38461  pmapglb2xN  40587  paddval  40613  elpadd0  40624  diophrex  43547  hbtlem1  43891  hbtlem7  43893  tfsconcatb0  44112  mnuop23d  45017  ismnushort  45052  sprval  48269  sprsymrelfvlem  48280  sprsymrelfv  48284  sprsymrelfo  48287  prprval  48304