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

Theorem rexlimivv 3197
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 3153 . 2 (𝑥𝐴 → (∃𝑦𝐵 𝜑𝜓))
32rexlimiv 3146 1 (∃𝑥𝐴𝑦𝐵 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  wrex 3074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3075
This theorem is referenced by:  r19.29vva  3208  2reu5  3721  2reu4  4489  opelxp  5674  elinxp  5980  reuop  6250  opiota  7996  f1o2ndf1  8059  poseq  8095  soseq  8096  tfrlem5  8331  xpdom2  9018  1sdomOLD  9200  unxpdomlem3  9203  unfiOLD  9264  elfiun  9373  ttrcltr  9659  xpnum  9894  kmlem9  10101  nqereu  10872  distrlem5pr  10970  mulid1  11160  1re  11162  mul02  11340  cnegex  11343  recex  11794  creur  12154  creui  12155  cju  12156  elz2  12524  zaddcl  12550  qre  12885  qaddcl  12897  qnegcl  12898  qmulcl  12899  qreccl  12901  elpqb  12908  hash2prd  14381  elss2prb  14393  fundmge2nop0  14398  wrdl3s3  14858  replim  15008  prodmo  15826  odd2np1  16230  opoe  16252  omoe  16253  opeo  16254  omeo  16255  qredeu  16541  pythagtriplem1  16695  pcz  16760  4sqlem1  16827  4sqlem2  16828  4sqlem4  16831  mul4sq  16833  pmtr3ncom  19264  efgmnvl  19503  efgrelexlema  19538  ring1ne0  20022  txuni2  22932  tx2ndc  23018  blssioo  24174  tgioo  24175  ioorf  24953  ioorinv  24956  ioorcl  24957  dyaddisj  24976  mbfid  25015  elply  25572  vmacl  26483  efvmacl  26485  vmalelog  26569  2sqlem2  26782  mul2sq  26783  2sqlem7  26788  2sqnn0  26802  2sqreultblem  26812  pntibnd  26957  ostth  27003  scutf  27173  legval  27568  upgredgpr  28135  nbgr2vtx1edg  28340  cusgredg  28414  usgredgsscusgredg  28449  wwlksnwwlksnon  28902  n4cyclfrgr  29277  vdgn1frgrv2  29282  friendshipgt3  29384  lpni  29464  nsnlplig  29465  nsnlpligALT  29466  n0lpligALT  29468  ipasslem5  29819  ipasslem11  29824  hhssnv  30248  shscli  30301  shsleji  30354  shsidmi  30368  spansncvi  30636  superpos  31338  chirredi  31378  mdsymlem6  31392  rnmposs  31632  1fldgenq  32129  ccfldextdgrr  32396  cnre2csqima  32532  dya2icobrsiga  32916  dya2iocnrect  32921  dya2iocucvr  32924  sxbrsigalem2  32926  afsval  33324  satfv0  33992  satfrnmapom  34004  satfv0fun  34005  satf00  34008  sat1el2xp  34013  fmla0xp  34017  fmla1  34021  msubco  34165  elaltxp  34589  altxpsspw  34591  funtransport  34645  funray  34754  funline  34756  ellines  34766  linethru  34767  icoreresf  35852  icoreclin  35857  relowlssretop  35863  relowlpssretop  35864  itg2addnc  36161  isline  38231  sn-it0e0  40913  sn-mulid2  40933  sn-0tie0  40937  sn-mul02  40938  mzpcompact2lem  41103  sprvalpw  45746  sprvalpwn0  45749  prsprel  45753  prpair  45767  prprvalpw  45781  reuopreuprim  45792  nnsum3primesgbe  46058  nnsum4primesodd  46062  nnsum4primesoddALTV  46063  tgblthelfgott  46081  nnpw2pb  46747  2arymaptf1  46813
  Copyright terms: Public domain W3C validator