Theorem rexeq 3322

Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2138, ax-11 2155, and ax-12 2172. (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 2726	. . 3 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
2		anbi1 633	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐵 ∧ 𝜑)))
3	2	alexbii 1836	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
4	1, 3	sylbi 216	. 2 ⊢ (𝐴 = 𝐵 → (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑)))
5		df-rex 3072	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
6		df-rex 3072	. 2 ⊢ (∃𝑥 ∈ 𝐵 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐵 ∧ 𝜑))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397  ∀wal 1540   = wceq 1542  ∃wex 1782   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-rex 3072

This theorem is referenced by:  raleq  3323  rexeqi  3325  rexeqdv  3327  reueq1  3416  unieqOLD  4921  axrep6g  5294  exss  5464  qseq1  8757  pssnn  9168  1sdomOLD  9249  pssnnOLD  9265  indexfi  9360  supeq1  9440  bnd2  9888  dfac2b  10125  cflem  10241  cflecard  10248  cfeq0  10251  cfsuc  10252  cfflb  10254  cofsmo  10264  elwina  10681  eltskg  10745  rankcf  10772  elnp  10982  elnpi  10983  genpv  10994  xrsupsslem  13286  xrinfmsslem  13287  xrsupss  13288  xrinfmss  13289  hashge2el2difr  14442  cat1  18047  isdrs  18254  isipodrs  18490  neifval  22603  ishaus  22826  2ndc1stc  22955  1stcrest  22957  lly1stc  23000  isref  23013  islocfin  23021  tx1stc  23154  isust  23708  iscfilu  23793  met1stc  24030  iscfil  24782  noetasuplem4  27239  precsexlemcbv  27652  precsexlem3  27655  ishpg  28010  isgrpo  29750  chne0  30747  pstmfval  32876  dya2iocuni  33282  satfvsuc  34352  satf0suc  34367  sat1el2xp  34370  fmlasuc0  34375  altxpeq1  34945  altxpeq2  34946  elhf2  35147  bj-sngleq  35848  cover2g  36584  indexdom  36602  istotbnd  36637  pmapglb2xN  38643  paddval  38669  elpadd0  38680  diophrex  41513  hbtlem1  41865  hbtlem7  41867  tfsconcatb0  42094  mnuop23d  43025  ismnushort  43060  sprval  46147  sprsymrelfvlem  46158  sprsymrelfv  46162  sprsymrelfo  46165  prprval  46182