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

Theorem rexlimivv 3296
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 3288 . 2 (𝑥𝐴 → (∃𝑦𝐵 𝜑𝜓))
32rexlimiv 3284 1 (∃𝑥𝐴𝑦𝐵 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2107  wrex 3143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-ral 3147  df-rex 3148
This theorem is referenced by:  2reu5  3752  2reu4  4468  opelxp  5589  elinxp  5888  reuop  6141  opiota  7751  f1o2ndf1  7812  tfrlem5  8010  xpdom2  8604  1sdom  8713  unxpdomlem3  8716  unfi  8777  elfiun  8886  xpnum  9372  kmlem9  9576  nqereu  10343  distrlem5pr  10441  mulid1  10631  1re  10633  mul02  10810  cnegex  10813  recex  11264  creur  11624  creui  11625  cju  11626  elz2  11991  zaddcl  12014  qre  12345  qaddcl  12357  qnegcl  12358  qmulcl  12359  qreccl  12361  elpqb  12368  hash2prd  13826  elss2prb  13838  fundmge2nop0  13843  wrdl3s3  14319  replim  14468  prodmo  15282  odd2np1  15682  opoe  15704  omoe  15705  opeo  15706  omeo  15707  qredeu  15994  pythagtriplem1  16145  pcz  16209  4sqlem1  16276  4sqlem2  16277  4sqlem4  16280  mul4sq  16282  pmtr3ncom  18525  efgmnvl  18762  efgrelexlema  18797  ring1ne0  19263  txuni2  22091  tx2ndc  22177  blssioo  23320  tgioo  23321  ioorf  24091  ioorinv  24094  ioorcl  24095  dyaddisj  24114  mbfid  24153  elply  24702  vmacl  25611  efvmacl  25613  vmalelog  25697  2sqlem2  25910  mul2sq  25911  2sqlem7  25916  2sqnn0  25930  2sqreultblem  25940  pntibnd  26085  ostth  26131  legval  26286  upgredgpr  26843  nbgr2vtx1edg  27048  cusgredg  27122  usgredgsscusgredg  27157  wwlksnwwlksnon  27610  n4cyclfrgr  27986  vdgn1frgrv2  27991  friendshipgt3  28093  lpni  28173  nsnlplig  28174  nsnlpligALT  28175  n0lpligALT  28177  ipasslem5  28528  ipasslem11  28533  hhssnv  28957  shscli  29010  shsleji  29063  shsidmi  29077  spansncvi  29345  superpos  30047  chirredi  30087  mdsymlem6  30101  rnmposs  30336  ccfldextdgrr  30945  cnre2csqima  31042  dya2icobrsiga  31422  dya2iocnrect  31427  dya2iocucvr  31430  sxbrsigalem2  31432  afsval  31830  satfv0  32491  satfrnmapom  32503  satfv0fun  32504  satf00  32507  sat1el2xp  32512  fmla0xp  32516  fmla1  32520  msubco  32664  poseq  32981  soseq  32982  scutf  33159  elaltxp  33322  altxpsspw  33324  funtransport  33378  funray  33487  funline  33489  ellines  33499  linethru  33500  icoreresf  34504  icoreclin  34509  relowlssretop  34515  relowlpssretop  34516  itg2addnc  34815  isline  36744  mzpcompact2lem  39215  sprvalpw  43476  sprvalpwn0  43479  prsprel  43483  prpair  43497  prprvalpw  43511  reuopreuprim  43522  nnsum3primesgbe  43791  nnsum4primesodd  43795  nnsum4primesoddALTV  43796  tgblthelfgott  43814  nnpw2pb  44481
  Copyright terms: Public domain W3C validator