Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexeq Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 nfcv 2751 . 2 𝑥𝐴
2 nfcv 2751 . 2 𝑥𝐵
31, 2rexeqf 3112 1 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑))
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator