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

Theorem rexlimivv 3017
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 3012 . 2 (𝑥𝐴 → (∃𝑦𝐵 𝜑𝜓))
32rexlimiv 3008 1 (∃𝑥𝐴𝑦𝐵 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  wrex 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-ral 2900  df-rex 2901
This theorem is referenced by:  2reu5  3382  opelxp  5059  opiota  7095  f1o2ndf1  7149  tfrlem5  7340  xpdom2  7917  1sdom  8025  unxpdomlem3  8028  unfi  8089  elfiun  8196  xpnum  8637  kmlem9  8840  nqereu  9607  distrlem5pr  9705  mulid1  9893  1re  9895  mul02  10065  cnegex  10068  recex  10510  creur  10863  creui  10864  cju  10865  elz2  11229  zaddcl  11252  qre  11627  qaddcl  11638  qnegcl  11639  qmulcl  11640  qreccl  11642  hash2prd  13066  elss2prb  13075  wrdl3s3  13501  replim  13652  prodmo  14453  odd2np1  14851  opoe  14873  omoe  14874  opeo  14875  omeo  14876  qredeu  15158  pythagtriplem1  15307  pcz  15371  4sqlem1  15438  4sqlem2  15439  4sqlem4  15442  mul4sq  15444  pmtr3ncom  17666  efgmnvl  17898  efgrelexlema  17933  ring1ne0  18362  txuni2  21125  tx2ndc  21211  blssioo  22353  tgioo  22354  ioorf  23091  ioorinv  23094  ioorcl  23095  dyaddisj  23114  mbfid  23153  elply  23699  vmacl  24588  efvmacl  24590  vmalelog  24674  2sqlem2  24887  mul2sq  24888  2sqlem7  24893  pntibnd  25026  ostth  25072  legval  25224  usgrasscusgra  25804  el2wlksoton  26198  el2spthsoton  26199  n4cyclfrgra  26338  vdn0frgrav2  26343  vdgn0frgrav2  26344  vdn1frgrav2  26345  vdgn1frgrav2  26346  2spotmdisj  26388  friendshipgt3  26441  lpni  26515  ipasslem5  26867  ipasslem11  26872  hhssnv  27298  shscli  27353  shsleji  27406  shsidmi  27420  spansncvi  27688  superpos  28390  chirredi  28430  mdsymlem6  28444  rnmpt2ss  28649  cnre2csqima  29078  dya2icobrsiga  29458  dya2iocnrect  29463  dya2iocucvr  29466  sxbrsigalem2  29468  afsval  29795  msubco  30475  poseq  30787  soseq  30788  nofulllem5  30898  elaltxp  31045  altxpsspw  31047  funtransport  31101  funray  31210  funline  31212  ellines  31222  linethru  31223  icoreresf  32159  icoreclin  32164  relowlssretop  32170  relowlpssretop  32171  itg2addnc  32417  isline  33826  mzpcompact2lem  36115  2reu4  39622  nnsum3primesgbe  39992  nnsum4primesodd  39996  nnsum4primesoddALTV  39997  tgblthelfgott  40013  fundmge2nop0  40131  upgredgpr  40355  nbgr2vtx1edg  40553  uvtx2vtx1edg  40606  cusgredg  40627  usgredgsscusgredg  40656  n4cyclfrgr  41442  vdgn1frgrv2  41447  av-friendshipgt3  41533  nnpw2pb  42160
  Copyright terms: Public domain W3C validator