Theorem rexeq 3310

Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.) Remove usage of ax-10 2144, ax-11 2161, and ax-12 2178. (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 265	. 2 ⊢ (𝐴 = 𝐵 → (𝜑 ↔ 𝜑))
2	1	rexeqbi1dv 3308	1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1542  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-cleq 2730  df-ral 3058  df-rex 3059

This theorem is referenced by:  rexeqi  3314  rexeqdv  3316  unieqOLD  4805  exss  5318  qseq1  8367  pssnn  8760  1sdom  8793  pssnnOLD  8808  indexfi  8898  supeq1  8975  bnd2  9388  dfac2b  9623  cflem  9739  cflecard  9746  cfeq0  9749  cfsuc  9750  cfflb  9752  cofsmo  9762  elwina  10179  eltskg  10243  rankcf  10270  elnp  10480  elnpi  10481  genpv  10492  xrsupsslem  12776  xrinfmsslem  12777  xrsupss  12778  xrinfmss  12779  hashge2el2difr  13926  cat1  17462  isdrs  17653  isipodrs  17880  neifval  21843  ishaus  22066  2ndc1stc  22195  1stcrest  22197  lly1stc  22240  isref  22253  islocfin  22261  tx1stc  22394  isust  22948  iscfilu  23033  met1stc  23267  iscfil  24010  ishpg  26697  isgrpo  28424  chne0  29421  pstmfval  31410  dya2iocuni  31812  satfvsuc  32886  satf0suc  32901  sat1el2xp  32904  fmlasuc0  32909  noetasuplem4  33572  altxpeq1  33905  altxpeq2  33906  elhf2  34107  bj-sngleq  34769  cover2g  35485  indexdom  35504  istotbnd  35539  pmapglb2xN  37398  paddval  37424  elpadd0  37435  diophrex  40153  hbtlem1  40504  hbtlem7  40506  mnuop23d  41410  sprval  44449  sprsymrelfvlem  44460  sprsymrelfv  44464  sprsymrelfo  44467  prprval  44484