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

Theorem rexeqi 3323
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 3320 . 2 (𝐴 = 𝐵 → (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑))
31, 2ax-mp 5 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐵 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1541  wrex 3069
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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-rex 3070
This theorem is referenced by:  rexrab2  3692  rexprgf  4690  rextpg  4696  rexopabb  5521  rexxp  5834  elidinxpid  6034  elrid  6035  oarec  8545  brttrcl2  9691  ttrcltr  9693  rnttrcl  9699  wwlktovfo  14891  dvdsprmpweqnn  16800  4sqlem12  16871  pmatcollpw3fi1  22219  cmpfi  22841  txbas  23000  xkobval  23019  ustn0  23654  imasdsf1olem  23808  xpsdsval  23816  plyun0  25640  coeeu  25668  1cubr  26274  made0  27291  addsrid  27364  muls01  27482  mulsrid  27483  dfnbgr3  28460  wlkvtxedg  28766  wwlksn0  28982  eucrctshift  29361  adjbdln  31199  elunirnmbfm  33081  satfbrsuc  34188  fmla1  34209  satffunlem2lem2  34228  filnetlem4  35070  rexrabdioph  41303  fnwe2lem2  41564  fourierdlem70  44665  fourierdlem80  44675
  Copyright terms: Public domain W3C validator