Theorem rexeq 3305

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

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

This theorem is referenced by:  raleq  3306  rexeqi  3308  rexeqdv  3310  reueq1  3401  axrep6g  5265  exss  5443  qseq1  8780  pssnn  9187  1sdomOLD  9262  indexfi  9377  supeq1  9462  bnd2  9912  dfac2b  10150  cflem  10264  cflemOLD  10265  cflecard  10272  cfeq0  10275  cfsuc  10276  cfflb  10278  cofsmo  10288  elwina  10705  eltskg  10769  rankcf  10796  elnp  11006  elnpi  11007  genpv  11018  xrsupsslem  13328  xrinfmsslem  13329  xrsupss  13330  xrinfmss  13331  hashge2el2difr  14504  cat1  18115  isdrs  18318  isipodrs  18552  neifval  23042  ishaus  23265  2ndc1stc  23394  1stcrest  23396  lly1stc  23439  isref  23452  islocfin  23460  tx1stc  23593  isust  24147  iscfilu  24231  met1stc  24465  iscfil  25222  noetasuplem4  27705  precsexlemcbv  28165  precsexlem3  28168  ishpg  28743  isgrpo  30483  chne0  31480  rprmdvdsprod  33554  constrsuc  33777  constrcbvlem  33794  pstmfval  33932  dya2iocuni  34320  satfvsuc  35388  satf0suc  35403  sat1el2xp  35406  fmlasuc0  35411  altxpeq1  35996  altxpeq2  35997  elhf2  36198  bj-sngleq  36990  cover2g  37745  indexdom  37763  istotbnd  37798  pmapglb2xN  39796  paddval  39822  elpadd0  39833  diophrex  42765  hbtlem1  43114  hbtlem7  43116  tfsconcatb0  43335  mnuop23d  44257  ismnushort  44292  sprval  47460  sprsymrelfvlem  47471  sprsymrelfv  47475  sprsymrelfo  47478  prprval  47495