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

Theorem rexlimivv 3217
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 3212 . 2 (𝑥𝐴 → (∃𝑦𝐵 𝜑𝜓))
32rexlimiv 3208 1 (∃𝑥𝐴𝑦𝐵 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  wcel 2157  wrex 3090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006
This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-ral 3094  df-rex 3095
This theorem is referenced by:  2reu5  3614  opelxp  5348  elinxp  5644  opiota  7464  f1o2ndf1  7522  tfrlem5  7715  xpdom2  8297  1sdom  8405  unxpdomlem3  8408  unfi  8469  elfiun  8578  xpnum  9063  kmlem9  9268  nqereu  10039  distrlem5pr  10137  mulid1  10326  1re  10328  mul02  10504  cnegex  10507  recex  10951  creur  11306  creui  11307  cju  11308  elz2  11683  zaddcl  11707  qre  12038  qaddcl  12049  qnegcl  12050  qmulcl  12051  qreccl  12053  elpqb  12060  hash2prd  13506  elss2prb  13518  fundmge2nop0  13523  wrdl3s3  14048  replim  14197  prodmo  15003  odd2np1  15401  opoe  15423  omoe  15424  opeo  15425  omeo  15426  qredeu  15706  pythagtriplem1  15854  pcz  15918  4sqlem1  15985  4sqlem2  15986  4sqlem4  15989  mul4sq  15991  pmtr3ncom  18207  efgmnvl  18440  efgrelexlema  18477  ring1ne0  18907  txuni2  21697  tx2ndc  21783  blssioo  22926  tgioo  22927  ioorf  23681  ioorinv  23684  ioorcl  23685  dyaddisj  23704  mbfid  23743  elply  24292  vmacl  25196  efvmacl  25198  vmalelog  25282  2sqlem2  25495  mul2sq  25496  2sqlem7  25501  pntibnd  25634  ostth  25680  legval  25835  upgredgpr  26378  nbgr2vtx1edg  26588  cusgredg  26674  usgredgsscusgredg  26709  wwlksnwwlksnon  27202  n4cyclfrgr  27640  vdgn1frgrv2  27645  friendshipgt3  27783  lpni  27860  nsnlplig  27861  nsnlpligALT  27862  n0lpligALT  27864  ipasslem5  28215  ipasslem11  28220  hhssnv  28646  shscli  28701  shsleji  28754  shsidmi  28768  spansncvi  29036  superpos  29738  chirredi  29778  mdsymlem6  29792  rnmpt2ss  29991  cnre2csqima  30473  dya2icobrsiga  30854  dya2iocnrect  30859  dya2iocucvr  30862  sxbrsigalem2  30864  afsval  31269  msubco  31945  poseq  32266  soseq  32267  scutf  32432  elaltxp  32595  altxpsspw  32597  funtransport  32651  funray  32760  funline  32762  ellines  32772  linethru  32773  icoreresf  33698  icoreclin  33703  relowlssretop  33709  relowlpssretop  33710  itg2addnc  33952  isline  35760  mzpcompact2lem  38100  2reu4  41967  nnsum3primesgbe  42462  nnsum4primesodd  42466  nnsum4primesoddALTV  42467  tgblthelfgott  42485  sprvalpw  42529  sprvalpwn0  42532  prsprel  42536  nnpw2pb  43180
  Copyright terms: Public domain W3C validator