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

Theorem 2rexbii 3037
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 3036 . 2 (∃𝑦𝐵 𝜑 ↔ ∃𝑦𝐵 𝜓)
32rexbii 3036 1 (∃𝑥𝐴𝑦𝐵 𝜑 ↔ ∃𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wrex 2909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-rex 2914
This theorem is referenced by:  rexnal3  3039  ralnex2  3040  ralnex3  3041  3reeanv  3102  addcompr  9803  mulcompr  9805  4fvwrd4  12416  ntrivcvgmul  14578  prodmo  14610  pythagtriplem2  15465  pythagtrip  15482  isnsgrp  17228  efgrelexlemb  18103  ordthaus  21128  regr1lem2  21483  fmucndlem  22035  dfcgra2  25655  axpasch  25755  axeuclid  25777  axcontlem4  25781  umgr2edg1  26030  frgrwopreglem5  27077  xrofsup  29418  poseq  31504  altopelaltxp  31778  brsegle  31910  mzpcompact2lem  36833  sbc4rex  36872  7rexfrabdioph  36883  expdiophlem1  37107  fourierdlem42  39703  ldepslinc  41616
  Copyright terms: Public domain W3C validator