Theorem rexeq 3343

Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2137, ax-11 2154, and ax-12 2171. (Revised by Steven Nguyen, 30-Apr-2023.)

Assertion

Ref	Expression
rexeq	⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rexeq

Step	Hyp	Ref	Expression
1		biidd 261	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜑))
2	1	rexeqbi1dv 3341	1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  ∃wrex 3065

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-ral 3069  df-rex 3070

This theorem is referenced by:  rexeqi  3347  rexeqdv  3349  unieqOLD  4851  axrep6g  5217  exss  5378  qseq1  8552  pssnn  8951  1sdom  9025  pssnnOLD  9040  indexfi  9127  supeq1  9204  bnd2  9651  dfac2b  9886  cflem  10002  cflecard  10009  cfeq0  10012  cfsuc  10013  cfflb  10015  cofsmo  10025  elwina  10442  eltskg  10506  rankcf  10533  elnp  10743  elnpi  10744  genpv  10755  xrsupsslem  13041  xrinfmsslem  13042  xrsupss  13043  xrinfmss  13044  hashge2el2difr  14195  cat1  17812  isdrs  18019  isipodrs  18255  neifval  22250  ishaus  22473  2ndc1stc  22602  1stcrest  22604  lly1stc  22647  isref  22660  islocfin  22668  tx1stc  22801  isust  23355  iscfilu  23440  met1stc  23677  iscfil  24429  ishpg  27120  isgrpo  28859  chne0  29856  pstmfval  31846  dya2iocuni  32250  satfvsuc  33323  satf0suc  33338  sat1el2xp  33341  fmlasuc0  33346  noetasuplem4  33939  altxpeq1  34275  altxpeq2  34276  elhf2  34477  bj-sngleq  35157  cover2g  35873  indexdom  35892  istotbnd  35927  pmapglb2xN  37786  paddval  37812  elpadd0  37823  diophrex  40597  hbtlem1  40948  hbtlem7  40950  mnuop23d  41884  ismnushort  41919  sprval  44931  sprsymrelfvlem  44942  sprsymrelfv  44946  sprsymrelfo  44949  prprval  44966