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

Theorem ralrimivva 2864
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 434 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ps ) )
32ralrimivv 2863 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1804   A.wral 2793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691
This theorem depends on definitions:  df-bi 185  df-an 371  df-ral 2798
This theorem is referenced by:  disjxiun  4434  otsndisj  4742  otiunsndisj  4743  swopo  4800  issod  4820  fcof1  6175  fliftfund  6196  soisores  6208  soisoi  6209  isocnv  6211  f1oiso  6232  oveqrspc2v  6304  caovclg  6452  caovcomg  6455  off  6539  caofrss  6558  caonncan  6563  dmmpt2g  6858  fnmpt2ovd  6863  fmpt2co  6868  poxp  6897  fvmpt2curryd  7002  smo11  7037  smoiso2  7042  omsmo  7305  qsdisj2  7391  eroprf  7411  dom2lem  7557  omxpenlem  7620  xpf1o  7681  unxpdomlem3  7728  fofinf1o  7803  dffi3  7893  supmo  7914  inf3lem6  8053  cantnf  8115  cantnfOLD  8137  rankxplim  8300  fseqenlem1  8408  fodomacn  8440  iunfictbso  8498  cofsmo  8652  infpssrlem5  8690  enfin2i  8704  fin23lem23  8709  fin23lem27  8711  fin23lem28  8723  compssiso  8757  ltordlem  10085  cju  10539  axdc4uzlem  12074  seqcaopr2  12125  seqhomo  12136  wrd2ind  12685  climcn2  13397  addcn2  13398  mulcn2  13400  o1of2  13417  isercolllem1  13469  fsum2dlem  13567  fsumcom2  13571  fprodser  13738  fprod2dlem  13766  fprodcom2  13770  isprm6  14232  crt  14290  eulerthlem2  14294  vdwlem12  14492  cshwsdisj  14565  imasaddfnlem  14907  imasvscafn  14916  mreexexd  15027  iscatd  15052  oppccomfpropd  15104  sectmon  15154  ssctr  15176  ssceq  15177  issubc3  15197  fullsubc  15198  fullresc  15199  isfuncd  15213  idfucl  15229  cofucl  15236  funcres2b  15245  fulloppc  15270  fthoppc  15271  idffth  15281  cofull  15282  cofth  15283  ressffth  15286  setcmon  15393  setcepi  15394  resssetc  15398  resscatc  15411  catciso  15413  evlfcl  15470  uncfcurf  15487  hofcl  15507  yonedalem3  15528  yonedainv  15529  yonffthlem  15530  yoniso  15533  isdrs2  15547  isposd  15564  pospropd  15743  poslubmo  15755  posglbmo  15756  mgmplusf  15860  opifismgm  15864  ismndd  15922  mndpropd  15925  issubmnd  15927  mhmpropd  15951  idmhm  15954  mhmf1o  15955  issubmd  15959  0mhm  15968  resmhm  15969  resmhm2  15970  resmhm2b  15971  mhmco  15972  submacs  15975  prdspjmhm  15977  pwsdiagmhm  15979  pwsco1mhm  15980  pwsco2mhm  15981  gsumwspan  15993  frmdsssubm  16008  frmdup1  16011  grpsubf  16096  mhmmnd  16171  mhmfmhm  16172  issubg4  16199  grpissubg  16200  isnsg3  16214  nsgacs  16216  0nsg  16225  nsgid  16226  isghmd  16255  ghmmhm  16256  idghm  16261  ghmnsgima  16269  ghmnsgpreima  16270  ghmf1  16274  ghmf1o  16275  gaid  16316  subgga  16317  gass  16318  gasubg  16319  cntzsubm  16352  cntrsubgnsg  16357  lactghmga  16408  symgfixf1  16441  odf1  16563  sylow1lem2  16598  sylow2blem2  16620  sylow3lem1  16626  lsmssv  16642  lsmidm  16661  pj1eu  16693  efglem  16713  efgtf  16719  efgred  16745  efgredeu  16749  frgpmhm  16762  frgpuptf  16767  frgpuplem  16769  mulgmhm  16815  ghmcmn  16819  invghm  16821  ablnsg  16832  gsum2d2lem  16980  gsum2d2  16981  gsumcom2  16982  dprd2d2  17072  ablfaclem2  17116  srglmhm  17165  srgrmhm  17166  isrhm2d  17356  kerf1hrm  17371  issubrg2  17428  subrgint  17430  islmodd  17497  lmodscaf  17513  lmodprop2d  17551  islssd  17561  islss4  17587  lssacs  17592  lsspropd  17642  islmhmd  17664  lmhmima  17672  lmhmpreima  17673  reslmhm  17677  lspextmo  17681  lsmcl  17708  pj1lmhm  17725  islbs2  17779  issubrngd2  17814  opprdomn  17929  abvn0b  17930  issubassa2  17973  mvrf1  18060  mplsubglem  18072  mplsubglemOLD  18074  mplsubrg  18081  mplcoe5lem  18109  mplcoe2  18111  mplind  18146  evlslem2  18159  evlseu  18164  ply1sclf1  18309  expmhm  18464  nn0srg  18465  prmirredlem  18501  prmirredlemOLD  18504  expghm  18507  expghmOLD  18508  mulgghm2  18509  mulgghm2OLD  18512  domnchr  18547  znf1o  18568  zntoslem  18573  znfld  18577  cygznlem3  18586  phlipf  18665  dsmmlss  18753  uvcf1  18801  frlmlbs  18809  lindff1  18833  lindfrn  18834  f1lindf  18835  mamucl  18881  mamuass  18882  mamudi  18883  mamudir  18884  mamuvs1  18885  mamuvs2  18886  matbas2d  18903  mamumat1cl  18919  mamulid  18921  mamurid  18922  mat1mhm  18964  dmatid  18975  dmatsubcl  18978  dmatsgrp  18979  dmatmulcl  18980  dmatsrng  18981  dmatcrng  18982  scmatscmiddistr  18988  scmatscm  18993  scmatsgrp  18999  scmatsrng  19000  scmatcrng  19001  scmatsgrp1  19002  scmatsrng1  19003  scmatf1  19011  scmatmhm  19014  mavmul0g  19033  mdet1  19081  mdetunilem9  19100  mdetuni0  19101  mdetmul  19103  madutpos  19122  smadiadetlem4  19149  1elcpmat  19194  cpmatacl  19195  cpmatmcl  19198  mat2pmatf1  19208  mat2pmatmul  19210  mat2pmat1  19211  mat2pmatlin  19214  m2cpm  19220  m2cpminvid  19232  m2cpminvid2  19234  decpmatmul  19251  pmatcollpw1  19255  monmatcollpw  19258  pmatcollpw  19260  pmatcollpw3lem  19262  pmatcollpwscmatlem2  19269  pm2mpf1  19278  mp2pm2mplem4  19288  pm2mpmhmlem2  19298  chp0mat  19325  chpidmat  19326  tgclb  19450  mretopd  19571  toponmre  19572  iscldtop  19574  ordtbaslem  19667  ordtbas2  19670  cnt0  19825  haust1  19831  cnhaus  19833  isreg2  19856  dishaus  19861  ordthaus  19863  dfcon2  19898  iuncon  19907  clscon  19909  2ndcomap  19937  dis2ndc  19939  llynlly  19956  restnlly  19961  restlly  19962  islly2  19963  llyidm  19967  nllyidm  19968  hausllycmp  19973  kgentopon  20017  txbas  20046  ptbasin2  20057  ptbasfi  20060  txcnp  20099  txcnmpt  20103  pthaus  20117  tx1stc  20129  xkococnlem  20138  xkococn  20139  cnmpt21  20150  qtoptop2  20178  qtopeu  20195  kqt0lem  20215  isr0  20216  regr1lem2  20219  kqreglem1  20220  kqreglem2  20221  kqnrmlem1  20222  kqnrmlem2  20223  nrmr0reg  20228  reghmph  20272  nrmhmph  20273  txswaphmeo  20284  qtophmeo  20296  fbun  20319  trfbas2  20322  isfil2  20335  infil  20342  trfil2  20366  filssufilg  20390  hausflim  20460  fclsnei  20498  fclsfnflim  20506  flimfnfcls  20507  ptcmplem1  20530  clssubg  20585  tgpconcomp  20589  qustgplem  20597  tsmsfbas  20604  utoptop  20715  iducn  20764  cstucnd  20765  isxmetd  20807  isxmet2d  20808  xmettpos  20830  prdsdsf  20848  prdsmet  20851  ressprdsds  20852  imasdsf1olem  20854  imasf1oxmet  20856  imasf1omet  20857  blfvalps  20864  xmetresbl  20918  metss2  20993  comet  20994  stdbdmet  20997  stdbdmopn  20999  methaus  21001  met2ndci  21003  metustfbasOLD  21046  metustfbas  21047  nrmmetd  21073  subgngp  21127  ngptgp  21128  sranlm  21171  nlmvscnlem1  21173  nlmvscn  21174  nrginvrcn  21178  lssnlm  21187  nghmcn  21230  qtopbaslem  21243  reconn  21311  xmetdcn2  21320  metdscn  21338  metnrm  21344  elcncf1di  21377  cncffvrn  21380  mulc1cncf  21387  cncfco  21389  reparphti  21475  tchcph  21658  ipcnlem1  21663  ipcn  21664  iscfil3  21690  bcthlem5  21745  rrxmet  21813  minveclem3  21822  minveclem7  21828  ovolicc2lem4  21909  dyadmbl  21987  volcn  21993  itg1addlem1  22077  itg1addlem2  22082  itg1addlem4  22084  mbfi1fseqlem1  22100  mbfi1fseqlem3  22102  mbfi1fseqlem4  22103  mbfi1fseqlem5  22104  dvmptfsum  22354  c1liplem1  22375  dvgt0lem2  22382  ftc1a  22416  ply1domn  22502  ply1divmo  22514  fta1b  22548  ig1peu  22550  coeeu  22600  plydivalg  22673  aaliou2b  22715  ulmss  22770  ulmcn  22772  efif1olem4  22910  efsubm  22916  logccv  23022  cvxcl  23292  basellem4  23335  fsumdvdscom  23439  musum  23445  dvdsmulf1o  23448  fsumdvdsmul  23449  dchrelbasd  23492  dchrmulcl  23502  dchrinv  23514  lgsqrlem2  23595  lgsdchr  23601  lgseisenlem2  23603  lgsquadlem1  23607  lgsquadlem2  23608  dchrisumlema  23651  dchrisumlem2  23653  chpdifbndlem2  23717  pntpbnd  23751  pntibndlem3  23755  axtgcont  23844  ercgrg  23886  idmot  23902  motco  23905  cnvmot  23906  motcgrg  23909  tgisline  23985  tghilbert1_2  23996  mirreu3  24013  mirmot  24033  ragperp  24072  foot  24074  mideu  24090  midf  24120  lmimot  24141  f1otrgds  24150  f1otrg  24152  f1otrge  24153  xmstrkgc  24167  brbtwn2  24186  axlowdimlem15  24237  axcontlem2  24246  axcontlem10  24254  eengtrkg  24266  eengtrkge  24267  usgraedgreu  24366  usgraidx2v  24371  wlknwwlkninj  24689  wlkiswwlkinj  24696  wwlkextinj  24708  clwwlkf1  24774  clwlkf1clwwlk  24828  2spotiundisj  25040  2spotmdisj  25046  numclwlk1lem2f1  25072  isgrp2d  25215  grpoinvf  25220  subgoablo  25291  ghgrplem2OLD  25347  ghabloOLD  25349  nvmf  25519  vacn  25582  nmcvcn  25583  smcnlem  25585  sspg  25619  ssps  25621  sspmlem  25623  0lno  25683  blocni  25698  sspph  25748  ipblnfi  25749  minvecolem7  25777  unopf1o  26813  cnvunop  26815  unoplin  26817  counop  26818  hmopadj2  26838  hmoplin  26839  bralnfn  26845  lnopeq0i  26904  hmops  26917  hmopm  26918  hmopco  26920  lnconi  26930  cnlnadjlem2  26965  adjmul  26989  adjadd  26990  cdjreui  27329  disjxpin  27425  off2  27459  f1od2  27525  xrofsup  27560  odutos  27629  abliso  27664  archiabllem1  27715  archiabllem2  27719  suborng  27783  xrge0slmod  27812  pstmxmet  27854  ofcf  28080  sibfof  28260  erdszelem4  28616  erdszelem9  28621  erdsze2lem2  28626  cnpcon  28653  pconcon  28654  txpcon  28655  ptpcon  28656  cvxpcon  28665  cvxscon  28666  iccllyscon  28673  cvmseu  28699  cvmliftmo  28707  cvmlift2lem5  28730  cvmlift2lem9  28734  mrsubff1  28852  elmrsubrn  28858  mrsubco  28859  msubff1  28894  mvhf1  28897  segconeu  29637  onsuct0  29882  fin2so  30016  heicant  30025  mblfinlem2  30028  ftc1anc  30074  fnessref  30151  neibastop1  30153  filnetlem3  30174  sdclem1  30212  isbnd3  30256  prdsbnd  30265  ismtycnv  30274  ismtyhmeolem  30276  ismtyres  30280  bfplem1  30294  bfplem2  30295  bfp  30296  rrnmet  30301  ismrer1  30310  iccbnd  30312  grpokerinj  30323  isdrngo2  30337  rngogrphom  30350  rngohomco  30353  rngoisocnv  30360  iscringd  30372  erprt  30590  nacsfix  30620  rmxypairf1o  30823  wepwsolem  30963  dnnumch3  30969  fnwe2  30975  mpaaeu  31075  idomsubgmo  31131  mon1psubm  31142  deg1mhm  31143  sumnnodd  31590  lptioo2  31591  lptioo1  31592  cncfshift  31630  cncfperiod  31635  dvnprodlem1  31697  fourierdlem42  31885  otiunsndisjX  32255  usgvincvadeu  32359  usgvincvadeuALT  32362  usgedgvadf1  32369  usgedgvadf1ALT  32372  ismgmd  32418  mgmhmpropd  32427  mgmhmf1o  32429  idmgmhm  32430  issubmgm2  32432  rabsubmgmd  32433  resmgmhm  32440  resmgmhm2  32441  resmgmhm2b  32442  mgmhmco  32443  submgmacs  32446  opmpt2ismgm  32448  mgmplusgiopALT  32471  isrnghm2d  32542  lidlmmgm  32558  2zlidl  32567  fthestrcsetc  32622  fullestrcsetc  32623  embedsetcestrclem  32629  fthsetcestrc  32637  fullsetcestrc  32638  rnghmsscmap2  32656  rnghmsscmap  32657  rnghmsubcsetclem2  32659  rhmsscmap2  32699  rhmsscmap  32700  rhmsubcsetclem2  32702  rhmsscrnghm  32706  rhmsubcrngclem2  32708  srhmsubc  32752  fldhmsubc  32760  rhmsubc  32766  srhmsubcOLD  32771  fldhmsubcOLD  32779  rhmsubcOLD  32785  lindslinindsimp1  32928  lfl0f  34669  lkrlss  34695  lshpsmreu  34709  linepsubN  35351  pmapsub  35367  lautcnv  35689  lautco  35696  idltrn  35749  cdleme50f1  36144  cdleme50laut  36148  istendod  36363  dihf11  36869  dih1dimatlem  36931  lcfl7N  37103  lcfrlem9  37152  mapd1o  37250  hdmapf1oN  37470  hgmapf1oN  37508
  Copyright terms: Public domain W3C validator