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

Theorem rexbiia 3174
 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 578 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32rexbii2 3173 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2111  ∃wrex 3071 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-rex 3076 This theorem is referenced by:  rexbii  3175  rexanid  3180  2rexbiia  3222  ceqsrexbv  3570  reu8  3649  f1oweALT  7683  reldm  7753  seqomlem2  8103  fofinf1o  8845  wdom2d  9090  unbndrank  9317  cfsmolem  9743  fin1a2lem5  9877  fin1a2lem6  9878  infm3  11649  wwlktovfo  14382  even2n  15756  smndex1mnd  18155  cycsubmel  18424  znf1o  20333  lmres  22014  ist1-2  22061  itg2monolem1  24464  lhop1lem  24726  elaa  25025  ulmcau  25103  reeff1o  25155  recosf1o  25240  chpo1ubb  26178  istrkg2ld  26367  wlkswwlksf1o  27778  wwlksnextsurj  27799  nmopnegi  29861  nmop0  29882  nmfn0  29883  adjbd1o  29981  atom1d  30249  abfmpunirn  30526  rearchi  31080  eulerpartgbij  31871  eulerpartlemgh  31877  subfacp1lem3  32673  dfrdg2  33300  noetainflem4  33541  heiborlem7  35570  qsresid  36057  eq0rabdioph  40135  elicores  42581  liminfpnfuz  42869  xlimpnfxnegmnf2  42911  fourierdlem70  43229  fourierdlem80  43239  ovolval3  43697  rexrsb  44082
 Copyright terms: Public domain W3C validator