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

Theorem rexbiia 3069
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 670 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32rexbii2 3068 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-rex 2947
This theorem is referenced by:  2rexbiia  3084  ceqsrexbv  3368  reu8  3435  f1oweALT  7194  reldm  7263  seqomlem2  7591  fofinf1o  8282  wdom2d  8526  unbndrank  8743  cfsmolem  9130  fin1a2lem5  9264  fin1a2lem6  9265  infm3  11020  wwlktovfo  13747  even2n  15113  znf1o  19948  lmres  21152  ist1-2  21199  itg2monolem1  23562  lhop1lem  23821  elaa  24116  ulmcau  24194  reeff1o  24246  recosf1o  24326  chpo1ubb  25215  istrkg2ld  25404  wlkpwwlkf1ouspgr  26833  wlknwwlksnsur  26844  wlkwwlksur  26851  wwlksnextsur  26863  nmopnegi  28952  nmop0  28973  nmfn0  28974  adjbd1o  29072  atom1d  29340  abfmpunirn  29580  rearchi  29970  eulerpartgbij  30562  eulerpartlemgh  30568  subfacp1lem3  31290  dfrdg2  31825  heiborlem7  33746  qsresid  34237  eq0rabdioph  37657  elicores  40078  fourierdlem70  40711  fourierdlem80  40721  ovolval3  41182  rexrsb  41490
  Copyright terms: Public domain W3C validator