MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralrimivva Structured version   Unicode version

Theorem ralrimivva 2853
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Contributed by Jeff Madsen, 19-Jun-2011.)
Hypothesis
Ref Expression
ralrimivva.1  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  ->  ps )
Assertion
Ref Expression
ralrimivva  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Distinct variable groups:    ph, x, y   
y, A
Allowed substitution hints:    ps( x, y)    A( x)    B( x, y)

Proof of Theorem ralrimivva
StepHypRef Expression
1 ralrimivva.1 . . 3  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  ->  ps )
21ex 435 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ps ) )
32ralrimivv 2852 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1870   A.wral 2782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751
This theorem depends on definitions:  df-bi 188  df-an 372  df-ral 2787
This theorem is referenced by:  disjxiun  4423  otsndisj  4726  otiunsndisj  4727  swopo  4785  issod  4805  fcof1  6200  fliftfund  6221  soisores  6233  soisoi  6234  isocnv  6236  f1oiso  6257  oveqrspc2v  6328  caovclg  6475  caovcomg  6478  off  6560  caofrss  6578  caonncan  6583  dmmpt2g  6880  fnmpt2ovd  6885  fmpt2co  6890  poxp  6919  fvmpt2curryd  7026  smo11  7091  smoiso2  7096  omsmo  7363  qsdisj2  7449  eroprf  7469  dom2lem  7616  omxpenlem  7679  xpf1o  7740  unxpdomlem3  7784  fofinf1o  7858  dffi3  7951  supmo  7972  inf3lem6  8138  cantnf  8197  rankxplim  8349  fseqenlem1  8453  fodomacn  8485  iunfictbso  8543  cofsmo  8697  infpssrlem5  8735  enfin2i  8749  fin23lem23  8754  fin23lem27  8756  fin23lem28  8768  compssiso  8802  ltordlem  10138  cju  10605  axdc4uzlem  12192  seqcaopr2  12246  seqhomo  12257  wrd2ind  12819  climcn2  13634  addcn2  13635  mulcn2  13637  o1of2  13654  isercolllem1  13706  fsum2dlem  13809  fsumcom2  13813  fprodser  13981  fprod2dlem  14012  fprodcom2  14016  isprm6  14628  crt  14686  eulerthlem2  14690  vdwlem12  14896  cshwsdisj  15023  imasaddfnlem  15376  imasvscafn  15385  mreexexd  15496  iscatd  15521  oppccomfpropd  15574  isofn  15622  sectmon  15629  ssctr  15672  ssceq  15673  catsubcat  15686  issubc3  15696  fullsubc  15697  fullresc  15698  isfuncd  15712  idfucl  15728  cofucl  15735  funcres2b  15744  fulloppc  15769  fthoppc  15770  idffth  15780  cofull  15781  cofth  15782  ressffth  15785  setcmon  15924  setcepi  15925  resssetc  15929  resscatc  15942  catciso  15944  fthestrcsetc  15977  fullestrcsetc  15978  embedsetcestrclem  15984  fthsetcestrc  15992  fullsetcestrc  15993  evlfcl  16049  uncfcurf  16066  hofcl  16086  yonedalem3  16107  yonedainv  16108  yonffthlem  16109  yoniso  16112  isdrs2  16126  isposd  16143  pospropd  16322  poslubmo  16334  posglbmo  16335  mgmplusf  16439  opifismgm  16443  ismndd  16501  mndpropd  16504  issubmnd  16506  mhmpropd  16530  idmhm  16533  mhmf1o  16534  issubmd  16538  0mhm  16547  resmhm  16548  resmhm2  16549  resmhm2b  16550  mhmco  16551  submacs  16554  prdspjmhm  16556  pwsdiagmhm  16558  pwsco1mhm  16559  pwsco2mhm  16560  gsumwspan  16572  frmdsssubm  16587  frmdup1  16590  grpsubf  16675  mhmmnd  16750  mhmfmhm  16751  issubg4  16778  grpissubg  16779  isnsg3  16793  nsgacs  16795  0nsg  16804  nsgid  16805  isghmd  16834  ghmmhm  16835  idghm  16840  ghmnsgima  16848  ghmnsgpreima  16849  ghmf1  16853  ghmf1o  16854  gaid  16895  subgga  16896  gass  16897  gasubg  16898  cntzsubm  16931  cntrsubgnsg  16936  lactghmga  16987  symgfixf1  17020  odf1  17142  sylow1lem2  17177  sylow2blem2  17199  sylow3lem1  17205  lsmssv  17221  lsmidm  17240  pj1eu  17272  efglem  17292  efgtf  17298  efgred  17324  efgredeu  17328  frgpmhm  17341  frgpuptf  17346  frgpuplem  17348  mulgmhm  17394  ghmcmn  17398  invghm  17400  ablnsg  17411  gsum2d2lem  17531  gsum2d2  17532  gsumcom2  17533  dprd2d2  17603  ablfaclem2  17645  srglmhm  17694  srgrmhm  17695  isrhm2d  17882  kerf1hrm  17897  issubrg2  17954  subrgint  17956  islmodd  18023  lmodscaf  18039  lmodprop2d  18076  islssd  18085  islss4  18111  lssacs  18116  lsspropd  18166  islmhmd  18188  lmhmima  18196  lmhmpreima  18197  reslmhm  18201  lspextmo  18205  lsmcl  18232  pj1lmhm  18249  islbs2  18303  issubrngd2  18338  opprdomn  18451  abvn0b  18452  issubassa2  18495  mvrf1  18575  mplsubglem  18584  mplsubrg  18590  mplcoe5lem  18617  mplcoe2  18619  mplind  18651  evlslem2  18661  evlseu  18665  ply1sclf1  18808  expmhm  18961  nn0srg  18962  prmirredlem  18986  expghm  18989  mulgghm2  18990  domnchr  19025  znf1o  19044  zntoslem  19049  znfld  19053  cygznlem3  19062  phlipf  19141  dsmmlss  19229  uvcf1  19272  frlmlbs  19277  lindff1  19300  lindfrn  19301  f1lindf  19302  mamucl  19348  mamuass  19349  mamudi  19350  mamudir  19351  mamuvs1  19352  mamuvs2  19353  matbas2d  19370  mamumat1cl  19386  mamulid  19388  mamurid  19389  mat1mhm  19431  dmatid  19442  dmatsubcl  19445  dmatsgrp  19446  dmatmulcl  19447  dmatsrng  19448  dmatcrng  19449  scmatscmiddistr  19455  scmatscm  19460  scmatsgrp  19466  scmatsrng  19467  scmatcrng  19468  scmatsgrp1  19469  scmatsrng1  19470  scmatf1  19478  scmatmhm  19481  mavmul0g  19500  mdet1  19548  mdetunilem9  19567  mdetuni0  19568  mdetmul  19570  madutpos  19589  smadiadetlem4  19616  1elcpmat  19661  cpmatacl  19662  cpmatmcl  19665  mat2pmatf1  19675  mat2pmatmul  19677  mat2pmat1  19678  mat2pmatlin  19681  m2cpm  19687  m2cpminvid  19699  m2cpminvid2  19701  decpmatmul  19718  pmatcollpw1  19722  monmatcollpw  19725  pmatcollpw  19727  pmatcollpw3lem  19729  pmatcollpwscmatlem2  19736  pm2mpf1  19745  mp2pm2mplem4  19755  pm2mpmhmlem2  19765  chp0mat  19792  chpidmat  19793  tgclb  19908  mretopd  20030  toponmre  20031  iscldtop  20033  ordtbaslem  20126  ordtbas2  20129  cnt0  20284  haust1  20290  cnhaus  20292  isreg2  20315  dishaus  20320  ordthaus  20322  dfcon2  20356  iuncon  20365  clscon  20367  2ndcomap  20395  dis2ndc  20397  llynlly  20414  restnlly  20419  restlly  20420  islly2  20421  llyidm  20425  nllyidm  20426  hausllycmp  20431  kgentopon  20475  txbas  20504  ptbasin2  20515  ptbasfi  20518  txcnp  20557  txcnmpt  20561  pthaus  20575  tx1stc  20587  xkococnlem  20596  xkococn  20597  cnmpt21  20608  qtoptop2  20636  qtopeu  20653  kqt0lem  20673  isr0  20674  regr1lem2  20677  kqreglem1  20678  kqreglem2  20679  kqnrmlem1  20680  kqnrmlem2  20681  nrmr0reg  20686  reghmph  20730  nrmhmph  20731  txswaphmeo  20742  qtophmeo  20754  fbun  20777  trfbas2  20780  isfil2  20793  infil  20800  trfil2  20824  filssufilg  20848  hausflim  20918  fclsnei  20956  fclsfnflim  20964  flimfnfcls  20965  ptcmplem1  20989  clssubg  21045  tgpconcomp  21049  qustgplem  21057  tsmsfbas  21064  utoptop  21171  iducn  21220  cstucnd  21221  isxmetd  21263  isxmet2d  21264  xmettpos  21286  prdsdsf  21304  prdsmet  21307  ressprdsds  21308  imasdsf1olem  21310  imasf1oxmet  21312  imasf1omet  21313  blfvalps  21320  xmetresbl  21374  metss2  21449  comet  21450  stdbdmet  21453  stdbdmopn  21455  methaus  21457  met2ndci  21459  metustfbas  21494  nrmmetd  21511  subgngp  21565  ngptgp  21566  sranlm  21609  nlmvscnlem1  21611  nlmvscn  21612  nrginvrcn  21616  lssnlm  21625  nghmcn  21668  qtopbaslem  21681  reconn  21748  xmetdcn2  21757  metdscn  21775  metnrm  21781  elcncf1di  21814  cncffvrn  21817  mulc1cncf  21824  cncfco  21826  reparphti  21912  tchcph  22095  ipcnlem1  22100  ipcn  22101  iscfil3  22127  bcthlem5  22180  rrxmet  22246  minveclem3  22255  minveclem7  22261  ovolicc2lem4  22342  dyadmbl  22426  volcn  22432  itg1addlem1  22518  itg1addlem2  22523  itg1addlem4  22525  mbfi1fseqlem1  22541  mbfi1fseqlem3  22543  mbfi1fseqlem4  22544  mbfi1fseqlem5  22545  dvmptfsum  22795  c1liplem1  22816  dvgt0lem2  22823  ftc1a  22857  ply1domn  22940  ply1divmo  22952  fta1b  22986  ig1peu  22988  coeeu  23038  plydivalg  23111  aaliou2b  23153  ulmss  23208  ulmcn  23210  efif1olem4  23350  efsubm  23356  logccv  23464  logbmpt  23581  logbfval  23583  cvxcl  23766  basellem4  23864  fsumdvdscom  23968  musum  23974  dvdsmulf1o  23977  fsumdvdsmul  23978  dchrelbasd  24021  dchrmulcl  24031  dchrinv  24043  lgsqrlem2  24124  lgsdchr  24130  lgseisenlem2  24132  lgsquadlem1  24136  lgsquadlem2  24137  dchrisumlema  24180  dchrisumlem2  24182  chpdifbndlem2  24246  pntpbnd  24280  pntibndlem3  24284  axtgcont  24371  ercgrg  24415  idmot  24433  motco  24436  cnvmot  24437  motcgrg  24440  tgisline  24522  tghilberti2  24533  mirreu3  24550  mirmot  24570  ragperp  24610  foot  24612  mideu  24628  midf  24665  lmimot  24687  trgcopyeu  24695  f1otrgds  24736  f1otrg  24738  f1otrge  24739  xmstrkgc  24753  brbtwn2  24772  axlowdimlem15  24823  axcontlem2  24832  axcontlem10  24840  eengtrkg  24852  eengtrkge  24853  usgraedgreu  24952  usgraidx2v  24957  wlknwwlkninj  25275  wlkiswwlkinj  25282  wwlkextinj  25294  clwwlkf1  25360  clwlkf1clwwlk  25414  2spotiundisj  25626  2spotmdisj  25632  numclwlk1lem2f1  25658  isgrp2d  25799  grpoinvf  25804  subgoablo  25875  ghgrplem2OLD  25931  ghabloOLD  25933  nvmf  26103  vacn  26166  nmcvcn  26167  smcnlem  26169  sspg  26203  ssps  26205  sspmlem  26207  0lno  26267  blocni  26282  sspph  26332  ipblnfi  26333  minvecolem7  26361  unopf1o  27395  cnvunop  27397  unoplin  27399  counop  27400  hmopadj2  27420  hmoplin  27421  bralnfn  27427  lnopeq0i  27486  hmops  27499  hmopm  27500  hmopco  27502  lnconi  27512  cnlnadjlem2  27547  adjmul  27571  adjadd  27572  cdjreui  27911  disjxpin  28028  off2  28073  f1od2  28143  xrofsup  28180  odutos  28253  abliso  28288  archiabllem1  28339  archiabllem2  28343  suborng  28408  xrge0slmod  28437  1smat1  28460  submateq  28465  madjusmdetlem3  28485  pstmxmet  28530  ofcf  28754  ldgenpisys  28818  rossros  28832  inelcarsg  28963  sibfof  28992  erdszelem4  29696  erdszelem9  29701  erdsze2lem2  29706  cnpcon  29732  pconcon  29733  txpcon  29734  ptpcon  29735  cvxpcon  29744  cvxscon  29745  iccllyscon  29752  cvmseu  29778  cvmliftmo  29786  cvmlift2lem5  29809  cvmlift2lem9  29813  mrsubff1  29931  elmrsubrn  29937  mrsubco  29938  msubff1  29973  mvhf1  29976  segconeu  30554  fnessref  30789  neibastop1  30791  filnetlem3  30812  onsuct0  30877  fin2so  31626  poimirlem4  31638  poimirlem13  31647  poimirlem14  31648  poimirlem26  31660  heicant  31669  mblfinlem2  31672  ftc1anc  31719  sdclem1  31766  isbnd3  31810  prdsbnd  31819  ismtycnv  31828  ismtyhmeolem  31830  ismtyres  31834  bfplem1  31848  bfplem2  31849  bfp  31850  rrnmet  31855  ismrer1  31864  iccbnd  31866  grpokerinj  31877  isdrngo2  31891  rngogrphom  31904  rngohomco  31907  rngoisocnv  31914  iscringd  31926  erprt  32143  lfl0f  32334  lkrlss  32360  lshpsmreu  32374  linepsubN  33016  pmapsub  33032  lautcnv  33354  lautco  33361  idltrn  33414  cdleme50f1  33809  cdleme50laut  33813  istendod  34028  dihf11  34534  dih1dimatlem  34596  lcfl7N  34768  lcfrlem9  34817  mapd1o  34915  hdmapf1oN  35135  hgmapf1oN  35173  nacsfix  35253  rmxypairf1o  35455  wepwsolem  35596  dnnumch3  35601  fnwe2  35607  mpaaeu  35705  idomsubgmo  35761  mon1psubm  35772  deg1mhm  35773  disjf1  37070  wessf1ornlem  37072  sumnnodd  37272  lptioo2  37273  lptioo1  37274  cncfshift  37313  cncfperiod  37318  dvnprodlem1  37380  fourierdlem42  37570  nnfoctbdjlem  37792  iccpartgt  38121  icceuelpart  38130  otiunsndisjX  38368  usgvincvadeu  38465  usgvincvadeuALT  38468  usgedgvadf1  38475  usgedgvadf1ALT  38478  ismgmd  38524  mgmhmpropd  38533  mgmhmf1o  38535  idmgmhm  38536  issubmgm2  38538  rabsubmgmd  38539  resmgmhm  38546  resmgmhm2  38547  resmgmhm2b  38548  mgmhmco  38549  submgmacs  38552  opmpt2ismgm  38555  mgmplusgiopALT  38578  isrnghm2d  38649  c0mgm  38657  c0mhm  38658  lidlmmgm  38673  2zlidl  38682  rnghmsscmap2  38723  rnghmsscmap  38724  rnghmsubcsetclem2  38726  rhmsscmap2  38769  rhmsscmap  38770  rhmsubcsetclem2  38772  rhmsscrnghm  38776  rhmsubcrngclem2  38778  srhmsubc  38826  fldhmsubc  38834  rhmsubc  38840  srhmsubcALTV  38845  fldhmsubcALTV  38853  rhmsubcALTV  38859  lindslinindsimp1  39000
  Copyright terms: Public domain W3C validator