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

Theorem ralrimivva 2821
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 440 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ps ) )
32ralrimivv 2820 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    e. wcel 1898   A.wral 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769
This theorem depends on definitions:  df-bi 190  df-an 377  df-ral 2754
This theorem is referenced by:  disjxiun  4413  otsndisj  4720  otiunsndisj  4721  swopo  4784  issod  4804  fcof1  6210  fliftfund  6231  soisores  6243  soisoi  6244  isocnv  6246  f1oiso  6267  oveqrspc2v  6338  caovclg  6488  caovcomg  6491  off  6573  caofrss  6591  caonncan  6596  dmmpt2g  6893  fnmpt2ovd  6898  fmpt2co  6906  poxp  6935  fvmpt2curryd  7044  smo11  7109  smoiso2  7114  omsmo  7381  qsdisj2  7467  eroprf  7487  dom2lem  7635  omxpenlem  7699  xpf1o  7760  unxpdomlem3  7804  fofinf1o  7878  dffi3  7971  supmo  7992  infmo  8037  inf3lem6  8164  cantnf  8224  rankxplim  8376  fseqenlem1  8481  fodomacn  8513  iunfictbso  8571  cofsmo  8725  infpssrlem5  8763  enfin2i  8777  fin23lem23  8782  fin23lem27  8784  fin23lem28  8796  compssiso  8830  ltordlem  10167  cju  10633  axdc4uzlem  12227  seqcaopr2  12281  seqhomo  12292  wrd2ind  12871  climcn2  13705  addcn2  13706  mulcn2  13708  o1of2  13725  isercolllem1  13777  fsum2dlem  13880  fsumcom2  13884  fprodser  14052  fprod2dlem  14083  fprodcom2  14087  isprm6  14715  crt  14775  eulerthlem2  14779  vdwlem12  14991  cshwsdisj  15118  imasaddfnlem  15483  imasvscafn  15492  mreexexd  15603  iscatd  15628  oppccomfpropd  15681  isofn  15729  sectmon  15736  ssctr  15779  ssceq  15780  catsubcat  15793  issubc3  15803  fullsubc  15804  fullresc  15805  isfuncd  15819  idfucl  15835  cofucl  15842  funcres2b  15851  fulloppc  15876  fthoppc  15877  idffth  15887  cofull  15888  cofth  15889  ressffth  15892  setcmon  16031  setcepi  16032  resssetc  16036  resscatc  16049  catciso  16051  fthestrcsetc  16084  fullestrcsetc  16085  embedsetcestrclem  16091  fthsetcestrc  16099  fullsetcestrc  16100  evlfcl  16156  uncfcurf  16173  hofcl  16193  yonedalem3  16214  yonedainv  16215  yonffthlem  16216  yoniso  16219  isdrs2  16233  isposd  16250  pospropd  16429  poslubmo  16441  posglbmo  16442  mgmplusf  16546  opifismgm  16550  ismndd  16608  mndpropd  16611  issubmnd  16613  mhmpropd  16637  idmhm  16640  mhmf1o  16641  issubmd  16645  0mhm  16654  resmhm  16655  resmhm2  16656  resmhm2b  16657  mhmco  16658  submacs  16661  prdspjmhm  16663  pwsdiagmhm  16665  pwsco1mhm  16666  pwsco2mhm  16667  gsumwspan  16679  frmdsssubm  16694  frmdup1  16697  grpsubf  16782  mhmmnd  16857  mhmfmhm  16858  issubg4  16885  grpissubg  16886  isnsg3  16900  nsgacs  16902  0nsg  16911  nsgid  16912  isghmd  16941  ghmmhm  16942  idghm  16947  ghmnsgima  16955  ghmnsgpreima  16956  ghmf1  16960  ghmf1o  16961  gaid  17002  subgga  17003  gass  17004  gasubg  17005  cntzsubm  17038  cntrsubgnsg  17043  lactghmga  17094  symgfixf1  17127  odf1  17262  sylow1lem2  17300  sylow2blem2  17322  sylow3lem1  17328  lsmssv  17344  lsmidm  17363  pj1eu  17395  efglem  17415  efgtf  17421  efgred  17447  efgredeu  17451  frgpmhm  17464  frgpuptf  17469  frgpuplem  17471  mulgmhm  17517  ghmcmn  17521  invghm  17523  ablnsg  17534  gsum2d2lem  17654  gsum2d2  17655  gsumcom2  17656  dprd2d2  17726  ablfaclem2  17768  srglmhm  17817  srgrmhm  17818  isrhm2d  18005  kerf1hrm  18020  issubrg2  18077  subrgint  18079  islmodd  18146  lmodscaf  18162  lmodprop2d  18199  islssd  18208  islss4  18234  lssacs  18239  lsspropd  18289  islmhmd  18311  lmhmima  18319  lmhmpreima  18320  reslmhm  18324  lspextmo  18328  lsmcl  18355  pj1lmhm  18372  islbs2  18426  issubrngd2  18461  opprdomn  18574  abvn0b  18575  issubassa2  18618  mvrf1  18698  mplsubglem  18707  mplsubrg  18713  mplcoe5lem  18740  mplcoe2  18742  mplind  18774  evlslem2  18784  evlseu  18788  ply1sclf1  18931  expmhm  19085  nn0srg  19086  prmirredlem  19113  expghm  19116  mulgghm2  19117  domnchr  19152  znf1o  19171  zntoslem  19176  znfld  19180  cygznlem3  19189  phlipf  19268  dsmmlss  19356  uvcf1  19399  frlmlbs  19404  lindff1  19427  lindfrn  19428  f1lindf  19429  mamucl  19475  mamuass  19476  mamudi  19477  mamudir  19478  mamuvs1  19479  mamuvs2  19480  matbas2d  19497  mamumat1cl  19513  mamulid  19515  mamurid  19516  mat1mhm  19558  dmatid  19569  dmatsubcl  19572  dmatsgrp  19573  dmatmulcl  19574  dmatsrng  19575  dmatcrng  19576  scmatscmiddistr  19582  scmatscm  19587  scmatsgrp  19593  scmatsrng  19594  scmatcrng  19595  scmatsgrp1  19596  scmatsrng1  19597  scmatf1  19605  scmatmhm  19608  mavmul0g  19627  mdet1  19675  mdetunilem9  19694  mdetuni0  19695  mdetmul  19697  madutpos  19716  smadiadetlem4  19743  1elcpmat  19788  cpmatacl  19789  cpmatmcl  19792  mat2pmatf1  19802  mat2pmatmul  19804  mat2pmat1  19805  mat2pmatlin  19808  m2cpm  19814  m2cpminvid  19826  m2cpminvid2  19828  decpmatmul  19845  pmatcollpw1  19849  monmatcollpw  19852  pmatcollpw  19854  pmatcollpw3lem  19856  pmatcollpwscmatlem2  19863  pm2mpf1  19872  mp2pm2mplem4  19882  pm2mpmhmlem2  19892  chp0mat  19919  chpidmat  19920  tgclb  20035  mretopd  20157  toponmre  20158  iscldtop  20160  ordtbaslem  20253  ordtbas2  20256  cnt0  20411  haust1  20417  cnhaus  20419  isreg2  20442  dishaus  20447  ordthaus  20449  dfcon2  20483  iuncon  20492  clscon  20494  2ndcomap  20522  dis2ndc  20524  llynlly  20541  restnlly  20546  restlly  20547  islly2  20548  llyidm  20552  nllyidm  20553  hausllycmp  20558  kgentopon  20602  txbas  20631  ptbasin2  20642  ptbasfi  20645  txcnp  20684  txcnmpt  20688  pthaus  20702  tx1stc  20714  xkococnlem  20723  xkococn  20724  cnmpt21  20735  qtoptop2  20763  qtopeu  20780  kqt0lem  20800  isr0  20801  regr1lem2  20804  kqreglem1  20805  kqreglem2  20806  kqnrmlem1  20807  kqnrmlem2  20808  nrmr0reg  20813  reghmph  20857  nrmhmph  20858  txswaphmeo  20869  qtophmeo  20881  fbun  20904  trfbas2  20907  isfil2  20920  infil  20927  trfil2  20951  filssufilg  20975  hausflim  21045  fclsnei  21083  fclsfnflim  21091  flimfnfcls  21092  ptcmplem1  21116  clssubg  21172  tgpconcomp  21176  qustgplem  21184  tsmsfbas  21191  utoptop  21298  iducn  21347  cstucnd  21348  isxmetd  21390  isxmet2d  21391  xmettpos  21413  prdsdsf  21431  prdsmet  21434  ressprdsds  21435  imasdsf1olem  21437  imasf1oxmet  21439  imasf1omet  21440  blfvalps  21447  xmetresbl  21501  metss2  21576  comet  21577  stdbdmet  21580  stdbdmopn  21582  methaus  21584  met2ndci  21586  metustfbas  21621  nrmmetd  21638  subgngp  21692  ngptgp  21693  sranlm  21736  nlmvscnlem1  21738  nlmvscn  21739  nrginvrcn  21743  lssnlm  21752  nghmcn  21815  qtopbaslem  21828  reconn  21895  xmetdcn2  21904  metdscn  21922  metdscnOLD  21937  metnrm  21943  elcncf1di  21976  cncffvrn  21979  mulc1cncf  21986  cncfco  21988  reparphti  22077  tchcph  22260  ipcnlem1  22265  ipcn  22266  iscfil3  22292  bcthlem5  22345  rrxmet  22411  minveclem3  22420  minveclem7  22426  minveclem3OLD  22432  minveclem7OLD  22438  ovolicc2lem4OLD  22522  ovolicc2lem4  22523  dyadmbl  22607  volcn  22613  itg1addlem1  22699  itg1addlem2  22704  itg1addlem4  22706  mbfi1fseqlem1  22722  mbfi1fseqlem3  22724  mbfi1fseqlem4  22725  mbfi1fseqlem5  22726  dvmptfsum  22976  c1liplem1  22997  dvgt0lem2  23004  ftc1a  23038  ply1domn  23121  ply1divmo  23135  fta1b  23169  ig1peu  23171  ig1peuOLD  23172  coeeu  23228  plydivalg  23301  aaliou2b  23346  ulmss  23401  ulmcn  23403  efif1olem4  23543  efsubm  23549  logccv  23657  logbmpt  23774  logbfval  23776  cvxcl  23959  basellem4  24059  fsumdvdscom  24163  musum  24169  dvdsmulf1o  24172  fsumdvdsmul  24173  dchrelbasd  24216  dchrmulcl  24226  dchrinv  24238  lgsqrlem2  24319  lgsdchr  24325  lgseisenlem2  24327  lgsquadlem1  24331  lgsquadlem2  24332  dchrisumlema  24375  dchrisumlem2  24377  chpdifbndlem2  24441  pntpbnd  24475  pntibndlem3  24479  axtgcont  24566  iscgrglt  24608  ercgrg  24611  idmot  24631  motco  24634  cnvmot  24635  motcgrg  24638  tgisline  24721  tghilberti2  24732  mirreu3  24748  mirmot  24769  ragperp  24811  foot  24813  mideu  24829  midf  24867  lmimot  24889  trgcopyeu  24897  f1otrgds  24948  f1otrg  24950  f1otrge  24951  xmstrkgc  24965  brbtwn2  24984  axlowdimlem15  25035  axcontlem2  25044  axcontlem10  25052  eengtrkg  25064  eengtrkge  25065  usgraedgreu  25164  usgraidx2v  25169  wlknwwlkninj  25488  wlkiswwlkinj  25495  wwlkextinj  25507  clwwlkf1  25573  clwlkf1clwwlk  25627  2spotiundisj  25839  2spotmdisj  25845  numclwlk1lem2f1  25871  isgrp2d  26012  grpoinvf  26017  subgoablo  26088  ghgrplem2OLD  26144  ghabloOLD  26146  nvmf  26316  vacn  26379  nmcvcn  26380  smcnlem  26382  sspg  26416  ssps  26418  sspmlem  26420  0lno  26480  blocni  26495  sspph  26545  ipblnfi  26546  minvecolem7  26574  minvecolem7OLD  26584  unopf1o  27618  cnvunop  27620  unoplin  27622  counop  27623  hmopadj2  27643  hmoplin  27644  bralnfn  27650  lnopeq0i  27709  hmops  27722  hmopm  27723  hmopco  27725  lnconi  27735  cnlnadjlem2  27770  adjmul  27794  adjadd  27795  cdjreui  28134  disjxpin  28247  off2  28291  f1od2  28358  xrofsup  28402  odutos  28473  abliso  28508  archiabllem1  28559  archiabllem2  28563  suborng  28627  xrge0slmod  28656  1smat1  28679  submateq  28684  madjusmdetlem3  28704  pstmxmet  28749  ofcf  28973  ldgenpisys  29037  rossros  29051  inelcarsg  29192  sibfof  29222  sitmf  29234  erdszelem4  29966  erdszelem9  29971  erdsze2lem2  29976  cnpcon  30002  pconcon  30003  txpcon  30004  ptpcon  30005  cvxpcon  30014  cvxscon  30015  iccllyscon  30022  cvmseu  30048  cvmliftmo  30056  cvmlift2lem5  30079  cvmlift2lem9  30083  mrsubff1  30201  elmrsubrn  30207  mrsubco  30208  msubff1  30243  mvhf1  30246  segconeu  30827  fnessref  31062  neibastop1  31064  filnetlem3  31085  onsuct0  31150  fin2so  31977  poimirlem4  31989  poimirlem13  31998  poimirlem14  31999  poimirlem26  32011  heicant  32020  mblfinlem2  32023  ftc1anc  32070  sdclem1  32117  isbnd3  32161  prdsbnd  32170  ismtycnv  32179  ismtyhmeolem  32181  ismtyres  32185  bfplem1  32199  bfplem2  32200  bfp  32201  rrnmet  32206  ismrer1  32215  iccbnd  32217  grpokerinj  32228  isdrngo2  32242  rngogrphom  32255  rngohomco  32258  rngoisocnv  32265  iscringd  32277  erprt  32490  lfl0f  32680  lkrlss  32706  lshpsmreu  32720  linepsubN  33362  pmapsub  33378  lautcnv  33700  lautco  33707  idltrn  33760  cdleme50f1  34155  cdleme50laut  34159  istendod  34374  dihf11  34880  dih1dimatlem  34942  lcfl7N  35114  lcfrlem9  35163  mapd1o  35261  hdmapf1oN  35481  hgmapf1oN  35519  nacsfix  35599  rmxypairf1o  35804  wepwsolem  35945  dnnumch3  35950  fnwe2  35956  mpaaeu  36061  idomsubgmo  36117  mon1psubm  36128  deg1mhm  36129  disjxp1  37449  disjf1  37495  wessf1ornlem  37497  projf1o  37512  sumnnodd  37748  lptioo2  37749  lptioo1  37750  cncfshift  37789  cncfperiod  37794  dvnprodlem1  37859  fourierdlem42  38050  fourierdlem42OLD  38051  nnfoctbdjlem  38331  isomennd  38390  iccpartgt  38779  icceuelpart  38788  otiunsndisjX  39046  usgredgreu  39345  uspgredg2vtxeu  39347  uspgredg2v  39351  usgredg2v  39354  usgvincvadeu  39990  usgvincvadeuALT  39993  usgedgvadf1  40000  usgedgvadf1ALT  40003  ismgmd  40049  mgmhmpropd  40058  mgmhmf1o  40060  idmgmhm  40061  issubmgm2  40063  rabsubmgmd  40064  resmgmhm  40071  resmgmhm2  40072  resmgmhm2b  40073  mgmhmco  40074  submgmacs  40077  opmpt2ismgm  40080  mgmplusgiopALT  40103  isrnghm2d  40174  c0mgm  40182  c0mhm  40183  lidlmmgm  40198  2zlidl  40207  rnghmsscmap2  40248  rnghmsscmap  40249  rnghmsubcsetclem2  40251  rhmsscmap2  40294  rhmsscmap  40295  rhmsubcsetclem2  40297  rhmsscrnghm  40301  rhmsubcrngclem2  40303  srhmsubc  40351  fldhmsubc  40359  rhmsubc  40365  srhmsubcALTV  40370  fldhmsubcALTV  40378  rhmsubcALTV  40384  lindslinindsimp1  40523
  Copyright terms: Public domain W3C validator