Theorem rexeq 3334

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ral 3068  df-rex 3069

This theorem is referenced by:  rexeqi  3338  rexeqdv  3340  unieqOLD  4848  exss  5372  qseq1  8510  pssnn  8913  1sdom  8955  pssnnOLD  8969  indexfi  9057  supeq1  9134  bnd2  9582  dfac2b  9817  cflem  9933  cflecard  9940  cfeq0  9943  cfsuc  9944  cfflb  9946  cofsmo  9956  elwina  10373  eltskg  10437  rankcf  10464  elnp  10674  elnpi  10675  genpv  10686  xrsupsslem  12970  xrinfmsslem  12971  xrsupss  12972  xrinfmss  12973  hashge2el2difr  14123  cat1  17728  isdrs  17934  isipodrs  18170  neifval  22158  ishaus  22381  2ndc1stc  22510  1stcrest  22512  lly1stc  22555  isref  22568  islocfin  22576  tx1stc  22709  isust  23263  iscfilu  23348  met1stc  23583  iscfil  24334  ishpg  27024  isgrpo  28760  chne0  29757  pstmfval  31748  dya2iocuni  32150  satfvsuc  33223  satf0suc  33238  sat1el2xp  33241  fmlasuc0  33246  noetasuplem4  33866  altxpeq1  34202  altxpeq2  34203  elhf2  34404  bj-sngleq  35084  cover2g  35800  indexdom  35819  istotbnd  35854  pmapglb2xN  37713  paddval  37739  elpadd0  37750  diophrex  40513  hbtlem1  40864  hbtlem7  40866  mnuop23d  41773  ismnushort  41808  sprval  44819  sprsymrelfvlem  44830  sprsymrelfv  44834  sprsymrelfo  44837  prprval  44854