Theorem rexeq 3359

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ∃wrex 3107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-rex 3112

This theorem is referenced by:  rexeqi  3363  rexeqdv  3365  unieqOLD  4812  exss  5320  qseq1  8326  1sdom  8705  pssnn  8720  indexfi  8816  supeq1  8893  bnd2  9306  dfac2b  9541  cflem  9657  cflecard  9664  cfeq0  9667  cfsuc  9668  cfflb  9670  cofsmo  9680  elwina  10097  eltskg  10161  rankcf  10188  elnp  10398  elnpi  10399  genpv  10410  xrsupsslem  12688  xrinfmsslem  12689  xrsupss  12690  xrinfmss  12691  hashge2el2difr  13835  isdrs  17536  isipodrs  17763  neifval  21704  ishaus  21927  2ndc1stc  22056  1stcrest  22058  lly1stc  22101  isref  22114  islocfin  22122  tx1stc  22255  isust  22809  iscfilu  22894  met1stc  23128  iscfil  23869  ishpg  26553  isgrpo  28280  chne0  29277  pstmfval  31249  dya2iocuni  31651  satfvsuc  32721  satf0suc  32736  sat1el2xp  32739  fmlasuc0  32744  noetalem3  33332  altxpeq1  33547  altxpeq2  33548  elhf2  33749  bj-sngleq  34403  cover2g  35153  indexdom  35172  istotbnd  35207  pmapglb2xN  37068  paddval  37094  elpadd0  37105  diophrex  39716  hbtlem1  40067  hbtlem7  40069  mnuop23d  40974  sprval  43996  sprsymrelfvlem  44007  sprsymrelfv  44011  sprsymrelfo  44014  prprval  44031