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

Theorem rexlimivv 3065
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.)
Hypothesis
Ref Expression
rexlimivv.1 ((𝑥𝐴𝑦𝐵) → (𝜑𝜓))
Assertion
Ref Expression
rexlimivv (∃𝑥𝐴𝑦𝐵 𝜑𝜓)
Distinct variable groups:   𝑥,𝑦,𝜓   𝑦,𝐴
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem rexlimivv
StepHypRef Expression
1 rexlimivv.1 . . 3 ((𝑥𝐴𝑦𝐵) → (𝜑𝜓))
21rexlimdva 3060 . 2 (𝑥𝐴 → (∃𝑦𝐵 𝜑𝜓))
32rexlimiv 3056 1 (∃𝑥𝐴𝑦𝐵 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947
This theorem is referenced by:  2reu5  3449  opelxp  5180  opiota  7273  f1o2ndf1  7330  tfrlem5  7521  xpdom2  8096  1sdom  8204  unxpdomlem3  8207  unfi  8268  elfiun  8377  xpnum  8815  kmlem9  9018  nqereu  9789  distrlem5pr  9887  mulid1  10075  1re  10077  mul02  10252  cnegex  10255  recex  10697  creur  11052  creui  11053  cju  11054  elz2  11432  zaddcl  11455  qre  11831  qaddcl  11842  qnegcl  11843  qmulcl  11844  qreccl  11846  hash2prd  13295  elss2prb  13307  fundmge2nop0  13312  wrdl3s3  13751  replim  13900  prodmo  14710  odd2np1  15112  opoe  15134  omoe  15135  opeo  15136  omeo  15137  qredeu  15419  pythagtriplem1  15568  pcz  15632  4sqlem1  15699  4sqlem2  15700  4sqlem4  15703  mul4sq  15705  pmtr3ncom  17941  efgmnvl  18173  efgrelexlema  18208  ring1ne0  18637  txuni2  21416  tx2ndc  21502  blssioo  22645  tgioo  22646  ioorf  23387  ioorinv  23390  ioorcl  23391  dyaddisj  23410  mbfid  23448  elply  23996  vmacl  24889  efvmacl  24891  vmalelog  24975  2sqlem2  25188  mul2sq  25189  2sqlem7  25194  pntibnd  25327  ostth  25373  legval  25524  upgredgpr  26082  nbgr2vtx1edg  26291  cusgredg  26376  usgredgsscusgredg  26411  wwlksnwwlksnon  26878  n4cyclfrgr  27271  vdgn1frgrv2  27276  friendshipgt3  27385  lpni  27462  nsnlplig  27463  nsnlpligALT  27464  n0lpligALT  27466  ipasslem5  27818  ipasslem11  27823  hhssnv  28249  shscli  28304  shsleji  28357  shsidmi  28371  spansncvi  28639  superpos  29341  chirredi  29381  mdsymlem6  29395  rnmpt2ss  29601  cnre2csqima  30085  dya2icobrsiga  30466  dya2iocnrect  30471  dya2iocucvr  30474  sxbrsigalem2  30476  afsval  30877  msubco  31554  poseq  31878  soseq  31879  scutf  32044  elaltxp  32207  altxpsspw  32209  funtransport  32263  funray  32372  funline  32374  ellines  32384  linethru  32385  icoreresf  33330  icoreclin  33335  relowlssretop  33341  relowlpssretop  33342  itg2addnc  33594  isline  35343  mzpcompact2lem  37631  2reu4  41511  nnsum3primesgbe  42005  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  tgblthelfgott  42028  sprvalpw  42055  sprvalpwn0  42058  prsprel  42062  nnpw2pb  42706
  Copyright terms: Public domain W3C validator