Theorem rexeq 3116

Description: Equality theorem for restricted existential quantifier. (Contributed by NM, 29-Oct-1995.)

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rexeq

Step	Hyp	Ref	Expression
1		nfcv 2751	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2751	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	rexeqf 3112	1 ⊢ (𝐴 = 𝐵 → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐵 𝜑))

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902

This theorem is referenced by:  rexeqi  3120  rexeqdv  3122  rexeqbi1dv  3124  unieq  4380  exss  4858  qseq1  7683  1sdom  8048  pssnn  8063  indexfi  8157  supeq1  8234  bnd2  8639  dfac2  8836  cflem  8951  cflecard  8958  cfeq0  8961  cfsuc  8962  cfflb  8964  cofsmo  8974  elwina  9387  eltskg  9451  rankcf  9478  elnp  9688  elnpi  9689  genpv  9700  xrsupsslem  12009  xrinfmsslem  12010  xrsupss  12011  xrinfmss  12012  hashge2el2difr  13118  isdrs  16757  isipodrs  16984  neifval  20713  ishaus  20936  2ndc1stc  21064  1stcrest  21066  lly1stc  21109  isref  21122  islocfin  21130  tx1stc  21263  isust  21817  iscfilu  21902  met1stc  22136  iscfil  22871  isgrpo  26735  chne0  27737  pstmfval  29267  dya2iocuni  29672  nobndlem2  31092  nobndlem8  31098  altxpeq1  31250  altxpeq2  31251  elhf2  31452  bj-sngleq  32148  cover2g  32679  indexdom  32699  istotbnd  32738  pmapglb2xN  34076  paddval  34102  elpadd0  34113  diophrex  36357  hbtlem1  36712  hbtlem7  36714