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

Theorem ralrimivva 2720
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 423 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ps ) )
32ralrimivv 2719 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1715   A.wral 2628
This theorem is referenced by:  disjxiun  4122  swopo  4427  issod  4447  fcof1  5920  fliftfund  5935  soisores  5947  soisoi  5948  isocnv  5950  f1oiso  5971  caovclg  6139  caovcomg  6142  off  6220  caofrss  6237  caonncan  6242  fmpt2co  6330  poxp  6355  smo11  6523  smoiso2  6528  omsmo  6794  qsdisj2  6879  eroprf  6899  dom2lem  7044  omxpenlem  7106  xpf1o  7166  unxpdomlem3  7212  fofinf1o  7284  dffi3  7331  supmo  7350  inf3lem6  7481  cantnf  7542  rankxplim  7696  fseqenlem1  7798  fodomacn  7830  iunfictbso  7888  cofsmo  8042  infpssrlem5  8080  enfin2i  8094  fin23lem23  8099  fin23lem27  8101  fin23lem28  8113  compssiso  8147  ltordlem  9445  cju  9889  axdc4uzlem  11208  seqcaopr2  11246  seqhomo  11257  climcn2  12273  addcn2  12274  mulcn2  12276  o1of2  12293  isercolllem1  12345  fsum2dlem  12441  fsumcom2  12445  isprm6  12996  crt  13054  eulerthlem2  13058  vdwlem12  13247  imasaddfnlem  13640  imasvscafn  13649  mreexexd  13760  iscatd  13785  proplem  13802  oppccomfpropd  13840  sectmon  13890  ssctr  13912  ssceq  13913  issubc3  13933  fullsubc  13934  fullresc  13935  isfuncd  13949  idfucl  13965  cofucl  13972  funcres2b  13981  fulloppc  14006  fthoppc  14007  idffth  14017  cofull  14018  cofth  14019  ressffth  14022  setcmon  14129  setcepi  14130  resssetc  14134  resscatc  14147  catciso  14149  evlfcl  14206  uncfcurf  14223  hofcl  14243  yonedalem3  14264  yonedainv  14265  yonffthlem  14266  yoniso  14269  isdrs2  14283  isposd  14299  pospropd  14448  poslubmo  14460  mndplusf  14593  mndfo  14607  mndpropd  14608  issubmnd  14611  mhmpropd  14631  0mhm  14645  resmhm  14646  resmhm2  14647  resmhm2b  14648  mhmco  14649  submacs  14652  prdspjmhm  14653  pwsdiagmhm  14655  pwsco1mhm  14656  pwsco2mhm  14657  gsumwspan  14678  frmdsssubm  14693  frmdup1  14696  grpsubf  14755  issubg4  14848  isnsg3  14861  nsgacs  14863  0nsg  14872  nsgid  14873  isghmd  14902  ghmmhm  14903  idghm  14908  ghmnsgima  14916  ghmnsgpreima  14917  ghmf1  14921  ghmf1o  14922  gaid  14963  subgga  14964  gass  14965  gasubg  14966  lactghmga  14994  cntzsubm  15021  cntrsubgnsg  15026  odf1  15085  sylow1lem2  15120  sylow2blem2  15142  sylow3lem1  15148  lsmssv  15164  lsmidm  15183  pj1eu  15215  efglem  15235  efgtf  15241  efgred  15267  efgredeu  15271  frgpmhm  15284  frgpuptf  15289  frgpuplem  15291  mulgmhm  15337  invghm  15340  ablnsg  15349  gsum2d2lem  15434  gsum2d2  15435  gsumcom2  15436  dprd2d2  15489  ablfaclem2  15531  isrhm2d  15716  issubrg2  15775  subrgint  15777  islmodd  15843  lmodscaf  15859  lmodprop2d  15897  islssd  15903  islss4  15929  lssacs  15934  lsspropd  15984  islmhmd  16006  lmhmima  16014  lmhmpreima  16015  reslmhm  16019  lspextmo  16023  lsmcl  16046  pj1lmhm  16063  islbs2  16117  issubrngd2  16153  opprdomn  16252  abvn0b  16253  issubassa2  16294  mvrf1  16380  mplsubglem  16389  mplsubrg  16394  mplind  16453  evlslem2  16459  ply1sclf1  16574  prmirredlem  16663  expmhm  16666  expghm  16667  mulgghm2  16676  domnchr  16703  znf1o  16722  zntoslem  16727  znfld  16731  cygznlem3  16740  phlipf  16773  tgclb  16925  mretopd  17046  toponmre  17047  iscldtop  17049  ordtbaslem  17135  ordtbas2  17138  cnt0  17291  haust1  17297  cnhaus  17299  isreg2  17322  dishaus  17327  ordthaus  17329  dfcon2  17362  iuncon  17371  clscon  17373  2ndcomap  17401  dis2ndc  17403  llynlly  17420  restnlly  17425  restlly  17426  islly2  17427  llyidm  17431  nllyidm  17432  hausllycmp  17437  kgentopon  17450  txbas  17479  ptbasin2  17490  ptbasfi  17493  txcnp  17531  txcnmpt  17535  pthaus  17549  tx1stc  17561  xkococnlem  17570  xkococn  17571  cnmpt21  17582  qtoptop2  17607  qtopeu  17624  kqt0lem  17644  isr0  17645  regr1lem2  17648  kqreglem1  17649  kqreglem2  17650  kqnrmlem1  17651  kqnrmlem2  17652  nrmr0reg  17657  reghmph  17701  nrmhmph  17702  txswaphmeo  17713  qtophmeo  17725  fbun  17748  trfbas2  17751  isfil2  17764  infil  17771  trfil2  17795  filssufilg  17819  hausflim  17889  fclsnei  17927  fclsfnflim  17935  flimfnfcls  17936  ptcmplem1  17959  clssubg  18004  tgpconcomp  18008  divstgplem  18016  tsmsfbas  18023  isxmetd  18104  isxmet2d  18105  xmettpos  18126  prdsdsf  18144  prdsmet  18147  ressprdsds  18148  imasdsf1olem  18150  imasf1oxmet  18152  imasf1omet  18153  blfval  18160  xmetresbl  18196  metss2  18271  comet  18272  stdbdmet  18275  stdbdmopn  18277  methaus  18279  met2ndci  18281  nrmmetd  18310  subgngp  18364  ngptgp  18365  sranlm  18408  nlmvscnlem1  18410  nlmvscn  18411  nrginvrcn  18415  lssnlm  18424  nghmcn  18467  qtopbaslem  18480  reconn  18547  xmetdcn2  18556  metdscn  18574  metnrm  18580  elcncf1di  18613  cncffvrn  18616  mulc1cncf  18623  cncfco  18625  reparphti  18710  tchcph  18882  ipcnlem1  18887  ipcn  18888  iscfil3  18914  bcthlem5  18965  minveclem3  19008  minveclem7  19014  ovolicc2lem4  19094  dyadmbl  19170  volcn  19176  itg1addlem1  19262  itg1addlem2  19267  itg1addlem4  19269  mbfi1fseqlem1  19285  mbfi1fseqlem3  19287  mbfi1fseqlem4  19288  mbfi1fseqlem5  19289  dvmptfsum  19537  c1liplem1  19558  dvgt0lem2  19565  ftc1a  19599  evlseu  19615  ply1domn  19724  ply1divmo  19736  fta1b  19770  ig1peu  19772  coeeu  19822  plydivalg  19894  aaliou2b  19936  ulmss  19991  ulmcn  19993  efif1olem4  20125  logccv  20232  cvxcl  20501  basellem4  20544  fsumdvdscom  20648  musum  20654  dvdsmulf1o  20657  fsumdvdsmul  20658  dchrelbasd  20701  dchrmulcl  20711  dchrinv  20723  lgsqrlem2  20804  lgsdchr  20810  lgseisenlem2  20812  lgsquadlem1  20816  lgsquadlem2  20817  dchrisumlema  20860  dchrisumlem2  20862  chpdifbndlem2  20926  pntpbnd  20960  pntibndlem3  20964  usgraedgreu  21084  usgraidx2v  21089  isgrp2d  21334  grpoinvf  21339  subgoablo  21410  ghgrplem2  21466  ghablo  21468  nvmf  21638  vacn  21701  nmcvcn  21702  smcnlem  21704  sspg  21738  ssps  21740  sspmlem  21742  0lno  21802  blocni  21817  sspph  21867  ipblnfi  21868  minvecolem7  21896  unopf1o  22930  cnvunop  22932  unoplin  22934  counop  22935  hmopadj2  22955  hmoplin  22956  bralnfn  22962  lnopeq0i  23021  hmops  23034  hmopm  23035  hmopco  23037  lnconi  23047  cnlnadjlem2  23082  adjmul  23106  adjadd  23107  cdjreui  23446  off2  23578  xrofsup  23647  kerf1hrm  23748  utoptop  23858  iducn  23898  cstucnd  23899  metustfbas  23921  ofcf  24072  erdszelem4  24449  erdszelem9  24454  erdsze2lem2  24459  cnpcon  24485  pconcon  24486  txpcon  24487  ptpcon  24488  cvxpcon  24497  cvxscon  24498  iccllyscon  24505  cvmseu  24531  cvmliftmo  24539  cvmlift2lem5  24562  cvmlift2lem9  24566  fprodser  24844  brbtwn2  25360  axlowdimlem15  25411  axcontlem2  25420  axcontlem10  25428  segconeu  25461  onsuct0  25707  fnessref  25885  neibastop1  25900  filnetlem3  25921  r19.21aivvaOLD  25930  sdclem1  26045  isbnd3  26099  prdsbnd  26108  ismtycnv  26117  ismtyhmeolem  26119  ismtyres  26123  bfplem1  26137  bfplem2  26138  bfp  26139  rrnmet  26144  ismrer1  26153  iccbnd  26155  grpokerinj  26166  isdrngo2  26180  rngogrphom  26193  rngohomco  26196  rngoisocnv  26203  iscringd  26215  erprt  26332  nacsfix  26378  rmxypairf1o  26587  wepwsolem  26729  dnnumch3  26735  fnwe2  26741  dsmmlss  26801  uvcf1  26832  frlmlbs  26840  lindff1  26881  lindfrn  26882  f1lindf  26883  mpaaeu  26946  issubmd  26974  mamucl  27047  mamudiagcl  27048  mamulid  27049  mamurid  27050  mamuass  27051  mamudi  27052  mamudir  27053  mamuvs1  27054  mamuvs2  27055  idomsubgmo  27105  mon1psubm  27116  deg1mhm  27117  dmmpt2g  27574  lfl0f  29318  lkrlss  29344  lshpsmreu  29358  linepsubN  30000  pmapsub  30016  lautcnv  30338  lautco  30345  idltrn  30398  cdleme50f1  30791  cdleme50laut  30795  istendod  31010  dihf11  31516  dih1dimatlem  31578  lcfl7N  31750  lcfrlem9  31799  mapd1o  31897  hdmapf1oN  32117  hgmapf1oN  32155
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-11 1751
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1547  df-nf 1550  df-ral 2633
  Copyright terms: Public domain W3C validator