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

Theorem rexbiia 3092
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 3090 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wcel 2107  wrex 3070
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 3071
This theorem is referenced by:  rexbii  3094  rexanid  3096  2rexbiia  3206  ceqsrexbv  3607  reu8  3692  f1oweALT  7906  reldm  7977  seqomlem2  8398  fofinf1o  9274  wdom2d  9521  unbndrank  9783  cfsmolem  10211  fin1a2lem5  10345  fin1a2lem6  10346  infm3  12119  wwlktovfo  14853  even2n  16229  smndex1mnd  18725  cycsubmel  18998  znf1o  20974  lmres  22667  ist1-2  22714  itg2monolem1  25131  lhop1lem  25393  elaa  25692  ulmcau  25770  reeff1o  25822  recosf1o  25907  chpo1ubb  26845  noetainflem4  27104  istrkg2ld  27444  wlkswwlksf1o  28866  wwlksnextsurj  28887  nmopnegi  30949  nmop0  30970  nmfn0  30971  adjbd1o  31069  atom1d  31337  abfmpunirn  31614  rearchi  32185  eulerpartgbij  33029  eulerpartlemgh  33035  subfacp1lem3  33833  dfrdg2  34426  heiborlem7  36322  qsresid  36832  eq0rabdioph  41142  elicores  43857  liminfpnfuz  44143  xlimpnfxnegmnf2  44185  fourierdlem70  44503  fourierdlem80  44513  ovolval3  44974  rexrsb  45418
  Copyright terms: Public domain W3C validator