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

Theorem ralrimivva 2803
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 432 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ps ) )
32ralrimivv 2802 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1826   A.wral 2732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712
This theorem depends on definitions:  df-bi 185  df-an 369  df-ral 2737
This theorem is referenced by:  disjxiun  4364  otsndisj  4666  otiunsndisj  4667  swopo  4724  issod  4744  fcof1  6091  fliftfund  6112  soisores  6124  soisoi  6125  isocnv  6127  f1oiso  6148  oveqrspc2v  6219  caovclg  6366  caovcomg  6369  off  6453  caofrss  6472  caonncan  6477  dmmpt2g  6772  fnmpt2ovd  6777  fmpt2co  6782  poxp  6811  fvmpt2curryd  6918  smo11  6953  smoiso2  6958  omsmo  7221  qsdisj2  7307  eroprf  7327  dom2lem  7474  omxpenlem  7537  xpf1o  7598  unxpdomlem3  7642  fofinf1o  7716  dffi3  7806  supmo  7826  inf3lem6  7964  cantnf  8025  cantnfOLD  8047  rankxplim  8210  fseqenlem1  8318  fodomacn  8350  iunfictbso  8408  cofsmo  8562  infpssrlem5  8600  enfin2i  8614  fin23lem23  8619  fin23lem27  8621  fin23lem28  8633  compssiso  8667  ltordlem  9995  cju  10448  axdc4uzlem  11995  seqcaopr2  12046  seqhomo  12057  wrd2ind  12614  climcn2  13417  addcn2  13418  mulcn2  13420  o1of2  13437  isercolllem1  13489  fsum2dlem  13587  fsumcom2  13591  fprodser  13758  fprod2dlem  13786  fprodcom2  13790  isprm6  14252  crt  14310  eulerthlem2  14314  vdwlem12  14512  cshwsdisj  14585  imasaddfnlem  14935  imasvscafn  14944  mreexexd  15055  iscatd  15080  oppccomfpropd  15133  isofn  15181  sectmon  15188  ssctr  15231  ssceq  15232  catsubcat  15245  issubc3  15255  fullsubc  15256  fullresc  15257  isfuncd  15271  idfucl  15287  cofucl  15294  funcres2b  15303  fulloppc  15328  fthoppc  15329  idffth  15339  cofull  15340  cofth  15341  ressffth  15344  setcmon  15483  setcepi  15484  resssetc  15488  resscatc  15501  catciso  15503  fthestrcsetc  15536  fullestrcsetc  15537  embedsetcestrclem  15543  fthsetcestrc  15551  fullsetcestrc  15552  evlfcl  15608  uncfcurf  15625  hofcl  15645  yonedalem3  15666  yonedainv  15667  yonffthlem  15668  yoniso  15671  isdrs2  15685  isposd  15702  pospropd  15881  poslubmo  15893  posglbmo  15894  mgmplusf  15998  opifismgm  16002  ismndd  16060  mndpropd  16063  issubmnd  16065  mhmpropd  16089  idmhm  16092  mhmf1o  16093  issubmd  16097  0mhm  16106  resmhm  16107  resmhm2  16108  resmhm2b  16109  mhmco  16110  submacs  16113  prdspjmhm  16115  pwsdiagmhm  16117  pwsco1mhm  16118  pwsco2mhm  16119  gsumwspan  16131  frmdsssubm  16146  frmdup1  16149  grpsubf  16234  mhmmnd  16309  mhmfmhm  16310  issubg4  16337  grpissubg  16338  isnsg3  16352  nsgacs  16354  0nsg  16363  nsgid  16364  isghmd  16393  ghmmhm  16394  idghm  16399  ghmnsgima  16407  ghmnsgpreima  16408  ghmf1  16412  ghmf1o  16413  gaid  16454  subgga  16455  gass  16456  gasubg  16457  cntzsubm  16490  cntrsubgnsg  16495  lactghmga  16546  symgfixf1  16579  odf1  16701  sylow1lem2  16736  sylow2blem2  16758  sylow3lem1  16764  lsmssv  16780  lsmidm  16799  pj1eu  16831  efglem  16851  efgtf  16857  efgred  16883  efgredeu  16887  frgpmhm  16900  frgpuptf  16905  frgpuplem  16907  mulgmhm  16953  ghmcmn  16957  invghm  16959  ablnsg  16970  gsum2d2lem  17115  gsum2d2  17116  gsumcom2  17117  dprd2d2  17206  ablfaclem2  17250  srglmhm  17299  srgrmhm  17300  isrhm2d  17490  kerf1hrm  17505  issubrg2  17562  subrgint  17564  islmodd  17631  lmodscaf  17647  lmodprop2d  17685  islssd  17695  islss4  17721  lssacs  17726  lsspropd  17776  islmhmd  17798  lmhmima  17806  lmhmpreima  17807  reslmhm  17811  lspextmo  17815  lsmcl  17842  pj1lmhm  17859  islbs2  17913  issubrngd2  17948  opprdomn  18063  abvn0b  18064  issubassa2  18107  mvrf1  18194  mplsubglem  18206  mplsubglemOLD  18208  mplsubrg  18215  mplcoe5lem  18243  mplcoe2  18245  mplind  18280  evlslem2  18293  evlseu  18298  ply1sclf1  18443  expmhm  18598  nn0srg  18599  prmirredlem  18623  expghm  18626  mulgghm2  18627  domnchr  18662  znf1o  18681  zntoslem  18686  znfld  18690  cygznlem3  18699  phlipf  18778  dsmmlss  18866  uvcf1  18912  frlmlbs  18917  lindff1  18940  lindfrn  18941  f1lindf  18942  mamucl  18988  mamuass  18989  mamudi  18990  mamudir  18991  mamuvs1  18992  mamuvs2  18993  matbas2d  19010  mamumat1cl  19026  mamulid  19028  mamurid  19029  mat1mhm  19071  dmatid  19082  dmatsubcl  19085  dmatsgrp  19086  dmatmulcl  19087  dmatsrng  19088  dmatcrng  19089  scmatscmiddistr  19095  scmatscm  19100  scmatsgrp  19106  scmatsrng  19107  scmatcrng  19108  scmatsgrp1  19109  scmatsrng1  19110  scmatf1  19118  scmatmhm  19121  mavmul0g  19140  mdet1  19188  mdetunilem9  19207  mdetuni0  19208  mdetmul  19210  madutpos  19229  smadiadetlem4  19256  1elcpmat  19301  cpmatacl  19302  cpmatmcl  19305  mat2pmatf1  19315  mat2pmatmul  19317  mat2pmat1  19318  mat2pmatlin  19321  m2cpm  19327  m2cpminvid  19339  m2cpminvid2  19341  decpmatmul  19358  pmatcollpw1  19362  monmatcollpw  19365  pmatcollpw  19367  pmatcollpw3lem  19369  pmatcollpwscmatlem2  19376  pm2mpf1  19385  mp2pm2mplem4  19395  pm2mpmhmlem2  19405  chp0mat  19432  chpidmat  19433  tgclb  19557  mretopd  19679  toponmre  19680  iscldtop  19682  ordtbaslem  19775  ordtbas2  19778  cnt0  19933  haust1  19939  cnhaus  19941  isreg2  19964  dishaus  19969  ordthaus  19971  dfcon2  20005  iuncon  20014  clscon  20016  2ndcomap  20044  dis2ndc  20046  llynlly  20063  restnlly  20068  restlly  20069  islly2  20070  llyidm  20074  nllyidm  20075  hausllycmp  20080  kgentopon  20124  txbas  20153  ptbasin2  20164  ptbasfi  20167  txcnp  20206  txcnmpt  20210  pthaus  20224  tx1stc  20236  xkococnlem  20245  xkococn  20246  cnmpt21  20257  qtoptop2  20285  qtopeu  20302  kqt0lem  20322  isr0  20323  regr1lem2  20326  kqreglem1  20327  kqreglem2  20328  kqnrmlem1  20329  kqnrmlem2  20330  nrmr0reg  20335  reghmph  20379  nrmhmph  20380  txswaphmeo  20391  qtophmeo  20403  fbun  20426  trfbas2  20429  isfil2  20442  infil  20449  trfil2  20473  filssufilg  20497  hausflim  20567  fclsnei  20605  fclsfnflim  20613  flimfnfcls  20614  ptcmplem1  20637  clssubg  20692  tgpconcomp  20696  qustgplem  20704  tsmsfbas  20711  utoptop  20822  iducn  20871  cstucnd  20872  isxmetd  20914  isxmet2d  20915  xmettpos  20937  prdsdsf  20955  prdsmet  20958  ressprdsds  20959  imasdsf1olem  20961  imasf1oxmet  20963  imasf1omet  20964  blfvalps  20971  xmetresbl  21025  metss2  21100  comet  21101  stdbdmet  21104  stdbdmopn  21106  methaus  21108  met2ndci  21110  metustfbasOLD  21153  metustfbas  21154  nrmmetd  21180  subgngp  21234  ngptgp  21235  sranlm  21278  nlmvscnlem1  21280  nlmvscn  21281  nrginvrcn  21285  lssnlm  21294  nghmcn  21337  qtopbaslem  21350  reconn  21418  xmetdcn2  21427  metdscn  21445  metnrm  21451  elcncf1di  21484  cncffvrn  21487  mulc1cncf  21494  cncfco  21496  reparphti  21582  tchcph  21765  ipcnlem1  21770  ipcn  21771  iscfil3  21797  bcthlem5  21852  rrxmet  21920  minveclem3  21929  minveclem7  21935  ovolicc2lem4  22016  dyadmbl  22094  volcn  22100  itg1addlem1  22184  itg1addlem2  22189  itg1addlem4  22191  mbfi1fseqlem1  22207  mbfi1fseqlem3  22209  mbfi1fseqlem4  22210  mbfi1fseqlem5  22211  dvmptfsum  22461  c1liplem1  22482  dvgt0lem2  22489  ftc1a  22523  ply1domn  22609  ply1divmo  22621  fta1b  22655  ig1peu  22657  coeeu  22707  plydivalg  22780  aaliou2b  22822  ulmss  22877  ulmcn  22879  efif1olem4  23017  efsubm  23023  logccv  23131  logbmpt  23246  logbfval  23248  cvxcl  23431  basellem4  23474  fsumdvdscom  23578  musum  23584  dvdsmulf1o  23587  fsumdvdsmul  23588  dchrelbasd  23631  dchrmulcl  23641  dchrinv  23653  lgsqrlem2  23734  lgsdchr  23740  lgseisenlem2  23742  lgsquadlem1  23746  lgsquadlem2  23747  dchrisumlema  23790  dchrisumlem2  23792  chpdifbndlem2  23856  pntpbnd  23890  pntibndlem3  23894  axtgcont  23983  ercgrg  24028  idmot  24044  motco  24047  cnvmot  24048  motcgrg  24051  tgisline  24127  tghilberti2  24138  mirreu3  24155  mirmot  24175  ragperp  24214  foot  24216  mideu  24232  midf  24262  lmimot  24283  f1otrgds  24293  f1otrg  24295  f1otrge  24296  xmstrkgc  24310  brbtwn2  24329  axlowdimlem15  24380  axcontlem2  24389  axcontlem10  24397  eengtrkg  24409  eengtrkge  24410  usgraedgreu  24509  usgraidx2v  24514  wlknwwlkninj  24832  wlkiswwlkinj  24839  wwlkextinj  24851  clwwlkf1  24917  clwlkf1clwwlk  24971  2spotiundisj  25183  2spotmdisj  25189  numclwlk1lem2f1  25215  isgrp2d  25354  grpoinvf  25359  subgoablo  25430  ghgrplem2OLD  25486  ghabloOLD  25488  nvmf  25658  vacn  25721  nmcvcn  25722  smcnlem  25724  sspg  25758  ssps  25760  sspmlem  25762  0lno  25822  blocni  25837  sspph  25887  ipblnfi  25888  minvecolem7  25916  unopf1o  26951  cnvunop  26953  unoplin  26955  counop  26956  hmopadj2  26976  hmoplin  26977  bralnfn  26983  lnopeq0i  27042  hmops  27055  hmopm  27056  hmopco  27058  lnconi  27068  cnlnadjlem2  27103  adjmul  27127  adjadd  27128  cdjreui  27467  disjxpin  27577  off2  27621  f1od2  27697  xrofsup  27735  odutos  27804  abliso  27839  archiabllem1  27890  archiabllem2  27894  suborng  27959  xrge0slmod  27988  pstmxmet  28030  ofcf  28251  inelcarsg  28438  sibfof  28465  erdszelem4  28827  erdszelem9  28832  erdsze2lem2  28837  cnpcon  28864  pconcon  28865  txpcon  28866  ptpcon  28867  cvxpcon  28876  cvxscon  28877  iccllyscon  28884  cvmseu  28910  cvmliftmo  28918  cvmlift2lem5  28941  cvmlift2lem9  28945  mrsubff1  29063  elmrsubrn  29069  mrsubco  29070  msubff1  29105  mvhf1  29108  segconeu  29814  onsuct0  30059  fin2so  30205  heicant  30214  mblfinlem2  30217  ftc1anc  30264  fnessref  30341  neibastop1  30343  filnetlem3  30364  sdclem1  30402  isbnd3  30446  prdsbnd  30455  ismtycnv  30464  ismtyhmeolem  30466  ismtyres  30470  bfplem1  30484  bfplem2  30485  bfp  30486  rrnmet  30491  ismrer1  30500  iccbnd  30502  grpokerinj  30513  isdrngo2  30527  rngogrphom  30540  rngohomco  30543  rngoisocnv  30550  iscringd  30562  erprt  30780  nacsfix  30810  rmxypairf1o  31012  wepwsolem  31153  dnnumch3  31159  fnwe2  31165  mpaaeu  31267  idomsubgmo  31323  mon1psubm  31334  deg1mhm  31335  sumnnodd  31802  lptioo2  31803  lptioo1  31804  cncfshift  31842  cncfperiod  31847  dvnprodlem1  31909  fourierdlem42  32097  otiunsndisjX  32622  usgvincvadeu  32723  usgvincvadeuALT  32726  usgedgvadf1  32733  usgedgvadf1ALT  32736  ismgmd  32782  mgmhmpropd  32791  mgmhmf1o  32793  idmgmhm  32794  issubmgm2  32796  rabsubmgmd  32797  resmgmhm  32804  resmgmhm2  32805  resmgmhm2b  32806  mgmhmco  32807  submgmacs  32810  opmpt2ismgm  32813  mgmplusgiopALT  32836  isrnghm2d  32907  c0mgm  32915  c0mhm  32916  lidlmmgm  32931  2zlidl  32940  rnghmsscmap2  32981  rnghmsscmap  32982  rnghmsubcsetclem2  32984  rhmsscmap2  33027  rhmsscmap  33028  rhmsubcsetclem2  33030  rhmsscrnghm  33034  rhmsubcrngclem2  33036  srhmsubc  33084  fldhmsubc  33092  rhmsubc  33098  srhmsubcALTV  33103  fldhmsubcALTV  33111  rhmsubcALTV  33117  lindslinindsimp1  33258  lfl0f  35207  lkrlss  35233  lshpsmreu  35247  linepsubN  35889  pmapsub  35905  lautcnv  36227  lautco  36234  idltrn  36287  cdleme50f1  36682  cdleme50laut  36686  istendod  36901  dihf11  37407  dih1dimatlem  37469  lcfl7N  37641  lcfrlem9  37690  mapd1o  37788  hdmapf1oN  38008  hgmapf1oN  38046
  Copyright terms: Public domain W3C validator