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

Theorem rexbiia 3034
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 668 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32rexbii2 3033 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wcel 1987  wrex 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-rex 2913
This theorem is referenced by:  2rexbiia  3049  ceqsrexbv  3324  reu8  3388  f1oweALT  7104  reldm  7171  seqomlem2  7498  fofinf1o  8192  wdom2d  8436  unbndrank  8656  cfsmolem  9043  fin1a2lem5  9177  fin1a2lem6  9178  infm3  10933  wwlktovfo  13642  even2n  14997  znf1o  19828  lmres  21023  ist1-2  21070  itg2monolem1  23436  lhop1lem  23693  elaa  23988  ulmcau  24066  reeff1o  24118  recosf1o  24198  chpo1ubb  25083  istrkg2ld  25272  wlkpwwlkf1ouspgr  26647  wlknwwlksnsur  26658  wlkwwlksur  26665  wwlksnextsur  26677  nmopnegi  28691  nmop0  28712  nmfn0  28713  adjbd1o  28811  atom1d  29079  abfmpunirn  29312  rearchi  29645  eulerpartgbij  30233  eulerpartlemgh  30239  subfacp1lem3  30899  dfrdg2  31429  heiborlem7  33275  eq0rabdioph  36847  elicores  39194  fourierdlem70  39721  fourierdlem80  39731  ovolval3  40189  rexrsb  40494
  Copyright terms: Public domain W3C validator