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

Theorem rexbiia 3188
Description: Inference adding restricted existential quantifier to both sides of an equivalence. (Contributed by NM, 26-Oct-1999.)
Hypothesis
Ref Expression
rexbiia.1 (𝑥𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rexbiia (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)

Proof of Theorem rexbiia
StepHypRef Expression
1 rexbiia.1 . . 3 (𝑥𝐴 → (𝜑𝜓))
21pm5.32i 556 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32rexbii2 3187 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wcel 2145  wrex 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-rex 3067
This theorem is referenced by:  2rexbiia  3203  ceqsrexbv  3487  reu8  3554  f1oweALT  7299  reldm  7368  seqomlem2  7699  fofinf1o  8397  wdom2d  8641  unbndrank  8869  cfsmolem  9294  fin1a2lem5  9428  fin1a2lem6  9429  infm3  11184  wwlktovfo  13911  even2n  15274  znf1o  20115  lmres  21325  ist1-2  21372  itg2monolem1  23737  lhop1lem  23996  elaa  24291  ulmcau  24369  reeff1o  24421  recosf1o  24502  chpo1ubb  25391  istrkg2ld  25580  wlkswwlksf1o  27013  wlknwwlksnsurOLD  27024  wlkwwlksurOLD  27032  wwlksnextsur  27044  nmopnegi  29164  nmop0  29185  nmfn0  29186  adjbd1o  29284  atom1d  29552  abfmpunirn  29792  rearchi  30182  eulerpartgbij  30774  eulerpartlemgh  30780  subfacp1lem3  31502  dfrdg2  32037  heiborlem7  33948  qsresid  34439  eq0rabdioph  37866  elicores  40278  fourierdlem70  40910  fourierdlem80  40920  ovolval3  41381  rexrsb  41689
  Copyright terms: Public domain W3C validator