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

Theorem rexbiia 3187
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 570 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32rexbii2 3186 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wcel 2155  wrex 3056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-rex 3061
This theorem is referenced by:  2rexbiia  3202  ceqsrexbv  3490  reu8  3561  f1oweALT  7350  reldm  7419  seqomlem2  7750  fofinf1o  8448  wdom2d  8692  unbndrank  8920  cfsmolem  9345  fin1a2lem5  9479  fin1a2lem6  9480  infm3  11236  wwlktovfo  13990  even2n  15350  znf1o  20172  lmres  21384  ist1-2  21431  itg2monolem1  23808  lhop1lem  24067  elaa  24362  ulmcau  24440  reeff1o  24492  recosf1o  24573  chpo1ubb  25461  istrkg2ld  25650  wlkswwlksf1o  27069  wlknwwlksnsurOLD  27080  wlkwwlksurOLD  27088  wwlksnextsur  27100  nmopnegi  29215  nmop0  29236  nmfn0  29237  adjbd1o  29335  atom1d  29603  abfmpunirn  29837  rearchi  30224  eulerpartgbij  30816  eulerpartlemgh  30822  subfacp1lem3  31544  dfrdg2  32076  heiborlem7  33970  qsresid  34457  eq0rabdioph  37950  elicores  40330  fourierdlem70  40962  fourierdlem80  40972  ovolval3  41433  rexrsb  41773
  Copyright terms: Public domain W3C validator