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

Theorem rexbiia 3089
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 573 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32rexbii2 3087 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wcel 2098  wrex 3067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-rex 3068
This theorem is referenced by:  rexbii  3091  rexanid  3093  2rexbiia  3213  ceqsrexbv  3644  reu8  3730  f1oweALT  7982  reldm  8054  seqomlem2  8478  fofinf1o  9359  wdom2d  9611  unbndrank  9873  cfsmolem  10301  fin1a2lem5  10435  fin1a2lem6  10436  infm3  12211  wwlktovfo  14949  even2n  16326  smndex1mnd  18869  cycsubmel  19162  znf1o  21492  lmres  23224  ist1-2  23271  itg2monolem1  25700  lhop1lem  25966  elaa  26271  ulmcau  26351  reeff1o  26404  recosf1o  26489  chpo1ubb  27434  noetainflem4  27693  0reno  28245  istrkg2ld  28284  wlkswwlksf1o  29710  wwlksnextsurj  29731  nmopnegi  31795  nmop0  31816  nmfn0  31817  adjbd1o  31915  atom1d  32183  abfmpunirn  32459  rearchi  33082  eulerpartgbij  34025  eulerpartlemgh  34031  subfacp1lem3  34825  dfrdg2  35424  heiborlem7  37323  qsresid  37829  cxpi11d  41945  eq0rabdioph  42227  elicores  44947  liminfpnfuz  45233  xlimpnfxnegmnf2  45275  fourierdlem70  45593  fourierdlem80  45603  ovolval3  46064  rexrsb  46509
  Copyright terms: Public domain W3C validator