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

Theorem rexbiia 3093
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 576 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32rexbii2 3091 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wcel 2107  wrex 3071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072
This theorem is referenced by:  rexbii  3095  rexanid  3097  2rexbiia  3216  ceqsrexbv  3643  reu8  3728  f1oweALT  7954  reldm  8025  seqomlem2  8446  fofinf1o  9323  wdom2d  9571  unbndrank  9833  cfsmolem  10261  fin1a2lem5  10395  fin1a2lem6  10396  infm3  12169  wwlktovfo  14905  even2n  16281  smndex1mnd  18787  cycsubmel  19071  znf1o  21091  lmres  22786  ist1-2  22833  itg2monolem1  25250  lhop1lem  25512  elaa  25811  ulmcau  25889  reeff1o  25941  recosf1o  26026  chpo1ubb  26964  noetainflem4  27223  istrkg2ld  27691  wlkswwlksf1o  29113  wwlksnextsurj  29134  nmopnegi  31196  nmop0  31217  nmfn0  31218  adjbd1o  31316  atom1d  31584  abfmpunirn  31855  rearchi  32430  eulerpartgbij  33309  eulerpartlemgh  33315  subfacp1lem3  34111  dfrdg2  34705  heiborlem7  36623  qsresid  37132  eq0rabdioph  41447  elicores  44181  liminfpnfuz  44467  xlimpnfxnegmnf2  44509  fourierdlem70  44827  fourierdlem80  44837  ovolval3  45298  rexrsb  45743
  Copyright terms: Public domain W3C validator