MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2exbii Unicode version

Theorem 2exbii 1668
Description: Inference adding two existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)
Hypothesis
Ref Expression
2exbii.1
Assertion
Ref Expression
2exbii

Proof of Theorem 2exbii
StepHypRef Expression
1 2exbii.1 . . 3
21exbii 1667 . 2
32exbii 1667 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  E.wex 1612
This theorem is referenced by:  3exbii  1669  3exdistr  1780  eeeanv  1989  ee4anv  1990  cbvex4v  2034  2sb5rf  2195  sbel2x  2203  2exsb  2213  2mo2  2372  2moOLD  2374  2eu4OLD  2381  2eu6OLD  2384  rexcomf  3017  reean  3024  ceqsex3v  3149  ceqsex4v  3150  ceqsex8v  3152  vtocl3  3163  copsexg  4737  copsexgOLD  4738  opelopabsbALT  4761  opabn0  4783  rabxp  5041  elxp3  5055  elvv  5063  elvvv  5064  copsex2gb  5118  elcnv2  5185  cnvuni  5194  xpdifid  5440  coass  5531  fununi  5659  dfmpt3  5708  dfoprab2  6343  dmoprab  6383  rnoprab  6385  mpt2mptx  6393  resoprab  6398  elrnmpt2res  6416  ov3  6439  ov6g  6440  uniuni  6609  oprabex3  6789  oeeu  7271  xpassen  7631  zorn2lem6  8902  ltresr  9538  axaddf  9543  axmulf  9544  hashfun  12495  5oalem7  26578  mpt2mptxf  27518  eulerpartlemgvv  28315  elima4  29209  wfrlem4  29346  brtxp2  29531  brpprod3a  29536  brpprod3b  29537  elfuns  29565  brcart  29582  brimg  29587  brapply  29588  brsuccf  29591  brrestrict  29599  dfrdg4  29600  ellines  29802  itg2addnclem3  30068  pm11.52  31292  2exanali  31293  pm11.6  31298  pm11.7  31302  stoweidlem35  31817  tpres  32554  mpt2mptx2  32924  opelopab4  33324  bnj600  33977  bnj916  33991  bnj983  34009  bnj986  34012  bnj996  34013  bnj1021  34022  bj-cbvex4vv  34308  dalem20  35417  dvhopellsm  36844  diblsmopel  36898
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator