Theorem rexeq 3406

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893  df-rex 3144

This theorem is referenced by:  rexeqi  3414  rexeqdv  3416  rexeqbi1dvOLD  3418  unieqOLD  4850  exss  5355  qseq1  8343  1sdom  8721  pssnn  8736  indexfi  8832  supeq1  8909  bnd2  9322  dfac2b  9556  cflem  9668  cflecard  9675  cfeq0  9678  cfsuc  9679  cfflb  9681  cofsmo  9691  elwina  10108  eltskg  10172  rankcf  10199  elnp  10409  elnpi  10410  genpv  10421  xrsupsslem  12701  xrinfmsslem  12702  xrsupss  12703  xrinfmss  12704  hashge2el2difr  13840  isdrs  17544  isipodrs  17771  neifval  21707  ishaus  21930  2ndc1stc  22059  1stcrest  22061  lly1stc  22104  isref  22117  islocfin  22125  tx1stc  22258  isust  22812  iscfilu  22897  met1stc  23131  iscfil  23868  ishpg  26545  isgrpo  28274  chne0  29271  pstmfval  31136  dya2iocuni  31541  satfvsuc  32608  satf0suc  32623  sat1el2xp  32626  fmlasuc0  32631  noetalem3  33219  altxpeq1  33434  altxpeq2  33435  elhf2  33636  bj-sngleq  34282  cover2g  35005  indexdom  35024  istotbnd  35062  pmapglb2xN  36923  paddval  36949  elpadd0  36960  diophrex  39392  hbtlem1  39743  hbtlem7  39745  mnuop23d  40622  sprval  43661  sprsymrelfvlem  43672  sprsymrelfv  43676  sprsymrelfo  43679  prprval  43696