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

Theorem rexeqi 3322
Description: Equality inference for restricted existential quantifier. (Contributed by Mario Carneiro, 23-Apr-2015.)
Hypothesis
Ref Expression
raleq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
rexeqi (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rexeqi
StepHypRef Expression
1 raleq1i.1 . 2 𝐴 = 𝐵
2 rexeq 3319 . 2 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑))
31, 2ax-mp 5 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1563  wrex 3089
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737
This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-rex 3090
This theorem is referenced by:  rexrab2  3666  rexprgf  4657  rextpg  4661  rexopabb  5503  rexxp  5819  elidinxpid  6038  elrid  6039  oarec  8535  brttrcl2  9671  ttrcltr  9673  rnttrcl  9679  wwlktovfo  14985  dvdsprmpweqnn  16935  4sqlem12  17006  pzriprnglem10  21600  pmatcollpw3fi1  22906  cmpfi  23526  txbas  23685  xkobval  23704  ustn0  24339  imasdsf1olem  24491  xpsdsval  24499  plyun0  26315  coeeu  26343  1cubr  26965  made0  28014  addsrid  28115  muls01  28263  mulsrid  28264  precsexlemcbv  28357  dfnbgr3  29597  wlkvtxedg  29902  wwlksn0  30121  eucrctshift  30503  adjbdln  32344  elunirnmbfm  34559  onvf1odlem2  35459  satfbrsuc  35729  fmla1  35750  satffunlem2lem2  35769  filnetlem4  36754  rexrabdioph  43383  fnwe2lem2  43640  fourierdlem70  46748  fourierdlem80  46758  dfclnbgr3  48446  stgr1  48581
  Copyright terms: Public domain W3C validator