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

Theorem ralrimivva 2636
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 2635 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 1685   A.wral 2544
This theorem is referenced by:  disjxiun  4021  swopo  4323  issod  4343  fcof1  5759  fliftfund  5774  soisores  5786  soisoi  5787  isocnv  5789  f1oiso  5810  caovclg  5974  caovcomg  5977  off  6055  caofrss  6072  caonncan  6077  fmpt2co  6164  poxp  6189  smo11  6377  smoiso2  6382  omsmo  6648  qsdisj2  6733  eroprf  6752  dom2lem  6897  omxpenlem  6959  xpf1o  7019  unxpdomlem3  7065  fofinf1o  7133  dffi3  7180  supmo  7199  inf3lem6  7330  cantnf  7391  rankxplim  7545  fseqenlem1  7647  fodomacn  7679  iunfictbso  7737  cofsmo  7891  infpssrlem5  7929  enfin2i  7943  fin23lem23  7948  fin23lem27  7950  fin23lem28  7962  compssiso  7996  ltordlem  9294  cju  9738  axdc4uzlem  11040  seqcaopr2  11078  seqhomo  11089  climcn2  12062  addcn2  12063  mulcn2  12065  o1of2  12082  isercolllem1  12134  fsum2dlem  12229  fsumcom2  12233  isprm6  12784  crt  12842  eulerthlem2  12846  vdwlem12  13035  imasaddfnlem  13426  imasvscafn  13435  mreexexd  13546  iscatd  13571  proplem  13588  oppccomfpropd  13626  sectmon  13676  ssctr  13698  ssceq  13699  issubc3  13719  fullsubc  13720  fullresc  13721  isfuncd  13735  idfucl  13751  cofucl  13758  funcres2b  13767  fulloppc  13792  fthoppc  13793  idffth  13803  cofull  13804  cofth  13805  ressffth  13808  setcmon  13915  setcepi  13916  resssetc  13920  resscatc  13933  catciso  13935  evlfcl  13992  uncfcurf  14009  hofcl  14029  yonedalem3  14050  yonedainv  14051  yonffthlem  14052  yoniso  14055  isdrs2  14069  isposd  14085  pospropd  14234  poslubmo  14246  mndplusf  14379  mndfo  14393  mndpropd  14394  issubmnd  14397  mhmpropd  14417  0mhm  14431  resmhm  14432  resmhm2  14433  resmhm2b  14434  mhmco  14435  submacs  14438  prdspjmhm  14439  pwsdiagmhm  14441  pwsco1mhm  14442  pwsco2mhm  14443  gsumwspan  14464  frmdsssubm  14479  frmdup1  14482  grpsubf  14541  issubg4  14634  isnsg3  14647  nsgacs  14649  0nsg  14658  nsgid  14659  isghmd  14688  ghmmhm  14689  idghm  14694  ghmnsgima  14702  ghmnsgpreima  14703  ghmf1  14707  ghmf1o  14708  gaid  14749  subgga  14750  gass  14751  gasubg  14752  lactghmga  14780  cntzsubm  14807  cntrsubgnsg  14812  odf1  14871  sylow1lem2  14906  sylow2blem2  14928  sylow3lem1  14934  lsmssv  14950  lsmidm  14969  pj1eu  15001  efglem  15021  efgtf  15027  efgred  15053  efgredeu  15057  frgpmhm  15070  frgpuptf  15075  frgpuplem  15077  mulgmhm  15123  invghm  15126  ablnsg  15135  gsum2d2lem  15220  gsum2d2  15221  gsumcom2  15222  dprd2d2  15275  ablfaclem2  15317  isrhm2d  15502  issubrg2  15561  subrgint  15563  islmodd  15629  lmodscaf  15645  lmodprop2d  15683  islssd  15689  islss4  15715  lssacs  15720  lsspropd  15770  islmhmd  15792  lmhmima  15800  lmhmpreima  15801  reslmhm  15805  lspextmo  15809  lsmcl  15832  pj1lmhm  15849  islbs2  15903  issubrngd2  15939  opprdomn  16038  abvn0b  16039  issubassa2  16080  mvrf1  16166  mplsubglem  16175  mplsubrg  16180  mplind  16239  evlslem2  16245  ply1sclf1  16360  prmirredlem  16442  expmhm  16445  expghm  16446  mulgghm2  16455  domnchr  16482  znf1o  16501  zntoslem  16506  znfld  16510  cygznlem3  16519  phlipf  16552  tgclb  16704  mretopd  16825  toponmre  16826  iscldtop  16828  ordtbaslem  16914  ordtbas2  16917  cnt0  17070  haust1  17076  cnhaus  17078  isreg2  17101  dishaus  17106  ordthaus  17108  dfcon2  17141  iuncon  17150  clscon  17152  2ndcomap  17180  dis2ndc  17182  llynlly  17199  restnlly  17204  restlly  17205  islly2  17206  llyidm  17210  nllyidm  17211  hausllycmp  17216  kgentopon  17229  txbas  17258  ptbasin2  17269  ptbasfi  17272  txcnp  17310  txcnmpt  17314  pthaus  17328  tx1stc  17340  xkococnlem  17349  xkococn  17350  cnmpt21  17361  qtoptop2  17386  qtopeu  17403  kqt0lem  17423  isr0  17424  regr1lem2  17427  kqreglem1  17428  kqreglem2  17429  kqnrmlem1  17430  kqnrmlem2  17431  nrmr0reg  17436  reghmph  17480  nrmhmph  17481  txswaphmeo  17492  qtophmeo  17504  fbun  17531  trfbas2  17534  isfil2  17547  infil  17554  trfil2  17578  filssufilg  17602  hausflim  17672  fclsnei  17710  fclsfnflim  17718  flimfnfcls  17719  ptcmplem1  17742  clssubg  17787  tgpconcomp  17791  divstgplem  17799  tsmsfbas  17806  isxmetd  17887  isxmet2d  17888  xmettpos  17909  prdsdsf  17927  prdsmet  17930  ressprdsds  17931  imasdsf1olem  17933  imasf1oxmet  17935  imasf1omet  17936  blfval  17943  xmetresbl  17979  metss2  18054  comet  18055  stdbdmet  18058  stdbdmopn  18060  methaus  18062  met2ndci  18064  nrmmetd  18093  subgngp  18147  ngptgp  18148  sranlm  18191  nlmvscnlem1  18193  nlmvscn  18194  nrginvrcn  18198  lssnlm  18207  nghmcn  18250  qtopbaslem  18263  reconn  18329  xmetdcn2  18338  metdscn  18356  metnrm  18362  elcncf1di  18395  cncffvrn  18398  mulc1cncf  18405  cncfco  18407  reparphti  18491  tchcph  18663  ipcnlem1  18668  ipcn  18669  iscfil3  18695  bcthlem5  18746  minveclem3  18789  minveclem7  18795  ovolicc2lem4  18875  dyadmbl  18951  volcn  18957  itg1addlem1  19043  itg1addlem2  19048  itg1addlem4  19050  mbfi1fseqlem1  19066  mbfi1fseqlem3  19068  mbfi1fseqlem4  19069  mbfi1fseqlem5  19070  dvmptfsum  19318  c1liplem1  19339  dvgt0lem2  19346  ftc1a  19380  evlseu  19396  ply1domn  19505  ply1divmo  19517  fta1b  19551  ig1peu  19553  coeeu  19603  plydivalg  19675  aaliou2b  19717  ulmss  19770  ulmcn  19772  efif1olem4  19903  logccv  20006  cvxcl  20275  basellem4  20317  fsumdvdscom  20421  musum  20427  dvdsmulf1o  20430  fsumdvdsmul  20431  dchrelbasd  20474  dchrmulcl  20484  dchrinv  20496  lgsqrlem2  20577  lgsdchr  20583  lgseisenlem2  20585  lgsquadlem1  20589  lgsquadlem2  20590  dchrisumlema  20633  dchrisumlem2  20635  chpdifbndlem2  20699  pntpbnd  20733  pntibndlem3  20737  isgrp2d  20896  grpoinvf  20901  subgoablo  20972  ghgrplem2  21028  ghablo  21030  nvmf  21198  vacn  21261  nmcvcn  21262  smcnlem  21264  sspg  21298  ssps  21300  sspmlem  21302  0lno  21362  blocni  21377  sspph  21427  ipblnfi  21428  minvecolem7  21456  unopf1o  22492  cnvunop  22494  unoplin  22496  counop  22497  hmopadj2  22517  hmoplin  22518  bralnfn  22524  lnopeq0i  22583  hmops  22596  hmopm  22597  hmopco  22599  lnconi  22609  cnlnadjlem2  22644  adjmul  22668  adjadd  22669  cdjreui  23008  erdszelem4  23132  erdszelem9  23137  erdsze2lem2  23142  cnpcon  23168  pconcon  23169  txpcon  23170  ptpcon  23171  cvxpcon  23180  cvxscon  23181  iccllyscon  23188  cvmseu  23214  cvmliftmo  23222  cvmlift2lem5  23245  cvmlift2lem9  23249  brbtwn2  23943  axlowdimlem15  23994  axcontlem2  24003  axcontlem10  24011  segconeu  24044  onsuct0  24290  toplat  24701  trooo  24805  rltrooo  24826  muldisc  24892  trnij  25026  sigadd  25060  fnmulcv  25095  icccon2  25111  icccon3  25112  icccon4  25113  idmon  25228  prismorcsetlemb  25324  setiscat  25390  fnessref  25704  neibastop1  25719  filnetlem3  25740  r19.21aivvaOLD  25749  sdclem1  25864  isbnd3  25919  prdsbnd  25928  ismtycnv  25937  ismtyhmeolem  25939  ismtyres  25943  bfplem1  25957  bfplem2  25958  bfp  25959  rrnmet  25964  ismrer1  25973  iccbnd  25975  grpokerinj  25986  isdrngo2  26000  rngogrphom  26013  rngohomco  26016  rngoisocnv  26023  iscringd  26035  erprt  26152  nacsfix  26198  rmxypairf1o  26407  wepwsolem  26549  dnnumch3  26555  fnwe2  26561  dsmmlss  26621  uvcf1  26652  frlmlbs  26660  lindff1  26701  lindfrn  26702  f1lindf  26703  mpaaeu  26766  issubmd  26794  mamucl  26867  mamudiagcl  26868  mamulid  26869  mamurid  26870  mamuass  26871  mamudi  26872  mamudir  26873  mamuvs1  26874  mamuvs2  26875  idomsubgmo  26925  mon1psubm  26936  deg1mhm  26937  dmmpt2g  27372  lfl0f  28538  lkrlss  28564  lshpsmreu  28578  linepsubN  29220  pmapsub  29236  lautcnv  29558  lautco  29565  idltrn  29618  cdleme50f1  30011  cdleme50laut  30015  istendod  30230  dihf11  30736  dih1dimatlem  30798  lcfl7N  30970  lcfrlem9  31019  mapd1o  31117  hdmapf1oN  31337  hgmapf1oN  31375
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-11 1716
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532  df-ral 2549
  Copyright terms: Public domain W3C validator