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

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

Proof of Theorem 2rexbii
StepHypRef Expression
1 2rexbii.1 . . 3 (𝜑𝜓)
21rexbii 3084 . 2 (∃𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 𝜓)
32rexbii 3084 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wrex 3060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-rex 3061
This theorem is referenced by:  rexnal3  3126  3reeanv  3218  2nreu  4438  poxp2  8149  poxp3  8156  poseq  8164  1sdom  9275  ttrcltr  9752  addcompr  11055  mulcompr  11057  4fvwrd4  13669  ntrivcvgmul  15901  prodmo  15933  pythagtriplem2  16814  pythagtrip  16831  cat1  18114  isnsgrp  18711  efgrelexlemb  19744  ordthaus  23376  regr1lem2  23732  fmucndlem  24284  madeval2  27874  dfcgra2  28754  axpasch  28872  axeuclid  28894  axcontlem4  28898  umgr2edg1  29144  wwlksnwwlksnon  29846  xrofsup  32674  satfvsucsuc  35206  satf0  35213  altopelaltxp  35813  brsegle  35945  fimgmcyclem  42223  fimgmcyc  42224  mzpcompact2lem  42445  sbc4rex  42483  7rexfrabdioph  42494  expdiophlem1  42716  fourierdlem42  45806  prpair  47109  ldepslinc  47928  sepnsepolem1  48291
  Copyright terms: Public domain W3C validator