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

Theorem 2rexbii 3024
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 3023 . 2 (∃𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 𝜓)
32rexbii 3023 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 195  wrex 2897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-rex 2902
This theorem is referenced by:  rexnal3  3026  ralnex2  3027  ralnex3  3028  3reeanv  3087  addcompr  9722  mulcompr  9724  4fvwrd4  12328  ntrivcvgmul  14473  prodmo  14505  pythagtriplem2  15360  pythagtrip  15377  isnsgrp  17111  efgrelexlemb  17986  ordthaus  20998  regr1lem2  21353  fmucndlem  21905  dfcgra2  25521  axpasch  25621  axeuclid  25643  axcontlem4  25647  frgrawopreglem5  26575  xrofsup  28923  poseq  30994  altopelaltxp  31253  brsegle  31385  mzpcompact2lem  36332  sbc4rex  36371  7rexfrabdioph  36382  expdiophlem1  36606  fourierdlem42  39042  umgr2edg1  40438  frgrwopreglem5  41485  ldepslinc  42092
  Copyright terms: Public domain W3C validator