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

Theorem 2rexbii 3242
Description: Inference adding two restricted existential quantifiers to both sides of an equivalence. (Contributed by NM, 11-Nov-1995.)
Hypothesis
Ref Expression
rexbii.1 (𝜑𝜓)
Assertion
Ref Expression
2rexbii (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝐴𝑦𝐵 𝜓)

Proof of Theorem 2rexbii
StepHypRef Expression
1 rexbii.1 . . 3 (𝜑𝜓)
21rexbii 3241 . 2 (∃𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 𝜓)
32rexbii 3241 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 209  wrex 3134
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 3139
This theorem is referenced by:  rexnal3  3253  3reeanv  3359  2nreu  4376  addcompr  10441  mulcompr  10443  4fvwrd4  13031  ntrivcvgmul  15258  prodmo  15290  pythagtriplem2  16152  pythagtrip  16169  isnsgrp  17905  efgrelexlemb  18876  ordthaus  21995  regr1lem2  22351  fmucndlem  22903  dfcgra2  26630  axpasch  26741  axeuclid  26763  axcontlem4  26767  umgr2edg1  27007  wwlksnwwlksnon  27707  xrofsup  30506  satfvsucsuc  32672  satf0  32679  poseq  33155  madeval2  33350  altopelaltxp  33497  brsegle  33629  mzpcompact2lem  39612  sbc4rex  39650  7rexfrabdioph  39661  expdiophlem1  39882  fourierdlem42  42721  prpair  43948  ldepslinc  44848
  Copyright terms: Public domain W3C validator