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

Theorem ralrimivva 2790
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 424 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ps ) )
32ralrimivv 2789 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725   A.wral 2697
This theorem is referenced by:  disjxiun  4201  swopo  4505  issod  4525  fcof1  6012  fliftfund  6027  soisores  6039  soisoi  6040  isocnv  6042  f1oiso  6063  caovclg  6231  caovcomg  6234  off  6312  caofrss  6329  caonncan  6334  fmpt2co  6422  poxp  6450  smo11  6618  smoiso2  6623  omsmo  6889  qsdisj2  6974  eroprf  6994  dom2lem  7139  omxpenlem  7201  xpf1o  7261  unxpdomlem3  7307  fofinf1o  7379  dffi3  7428  supmo  7449  inf3lem6  7580  cantnf  7641  rankxplim  7795  fseqenlem1  7897  fodomacn  7929  iunfictbso  7987  cofsmo  8141  infpssrlem5  8179  enfin2i  8193  fin23lem23  8198  fin23lem27  8200  fin23lem28  8212  compssiso  8246  ltordlem  9544  cju  9988  axdc4uzlem  11313  seqcaopr2  11351  seqhomo  11362  climcn2  12378  addcn2  12379  mulcn2  12381  o1of2  12398  isercolllem1  12450  fsum2dlem  12546  fsumcom2  12550  isprm6  13101  crt  13159  eulerthlem2  13163  vdwlem12  13352  imasaddfnlem  13745  imasvscafn  13754  mreexexd  13865  iscatd  13890  proplem  13907  oppccomfpropd  13945  sectmon  13995  ssctr  14017  ssceq  14018  issubc3  14038  fullsubc  14039  fullresc  14040  isfuncd  14054  idfucl  14070  cofucl  14077  funcres2b  14086  fulloppc  14111  fthoppc  14112  idffth  14122  cofull  14123  cofth  14124  ressffth  14127  setcmon  14234  setcepi  14235  resssetc  14239  resscatc  14252  catciso  14254  evlfcl  14311  uncfcurf  14328  hofcl  14348  yonedalem3  14369  yonedainv  14370  yonffthlem  14371  yoniso  14374  isdrs2  14388  isposd  14404  pospropd  14553  poslubmo  14565  mndplusf  14698  mndfo  14712  mndpropd  14713  issubmnd  14716  mhmpropd  14736  0mhm  14750  resmhm  14751  resmhm2  14752  resmhm2b  14753  mhmco  14754  submacs  14757  prdspjmhm  14758  pwsdiagmhm  14760  pwsco1mhm  14761  pwsco2mhm  14762  gsumwspan  14783  frmdsssubm  14798  frmdup1  14801  grpsubf  14860  issubg4  14953  isnsg3  14966  nsgacs  14968  0nsg  14977  nsgid  14978  isghmd  15007  ghmmhm  15008  idghm  15013  ghmnsgima  15021  ghmnsgpreima  15022  ghmf1  15026  ghmf1o  15027  gaid  15068  subgga  15069  gass  15070  gasubg  15071  lactghmga  15099  cntzsubm  15126  cntrsubgnsg  15131  odf1  15190  sylow1lem2  15225  sylow2blem2  15247  sylow3lem1  15253  lsmssv  15269  lsmidm  15288  pj1eu  15320  efglem  15340  efgtf  15346  efgred  15372  efgredeu  15376  frgpmhm  15389  frgpuptf  15394  frgpuplem  15396  mulgmhm  15442  invghm  15445  ablnsg  15454  gsum2d2lem  15539  gsum2d2  15540  gsumcom2  15541  dprd2d2  15594  ablfaclem2  15636  isrhm2d  15821  issubrg2  15880  subrgint  15882  islmodd  15948  lmodscaf  15964  lmodprop2d  15998  islssd  16004  islss4  16030  lssacs  16035  lsspropd  16085  islmhmd  16107  lmhmima  16115  lmhmpreima  16116  reslmhm  16120  lspextmo  16124  lsmcl  16147  pj1lmhm  16164  islbs2  16218  issubrngd2  16254  opprdomn  16353  abvn0b  16354  issubassa2  16395  mvrf1  16481  mplsubglem  16490  mplsubrg  16495  mplind  16554  evlslem2  16560  ply1sclf1  16672  prmirredlem  16765  expmhm  16768  expghm  16769  mulgghm2  16778  domnchr  16805  znf1o  16824  zntoslem  16829  znfld  16833  cygznlem3  16842  phlipf  16875  tgclb  17027  mretopd  17148  toponmre  17149  iscldtop  17151  ordtbaslem  17244  ordtbas2  17247  cnt0  17402  haust1  17408  cnhaus  17410  isreg2  17433  dishaus  17438  ordthaus  17440  dfcon2  17474  iuncon  17483  clscon  17485  2ndcomap  17513  dis2ndc  17515  llynlly  17532  restnlly  17537  restlly  17538  islly2  17539  llyidm  17543  nllyidm  17544  hausllycmp  17549  kgentopon  17562  txbas  17591  ptbasin2  17602  ptbasfi  17605  txcnp  17644  txcnmpt  17648  pthaus  17662  tx1stc  17674  xkococnlem  17683  xkococn  17684  cnmpt21  17695  qtoptop2  17723  qtopeu  17740  kqt0lem  17760  isr0  17761  regr1lem2  17764  kqreglem1  17765  kqreglem2  17766  kqnrmlem1  17767  kqnrmlem2  17768  nrmr0reg  17773  reghmph  17817  nrmhmph  17818  txswaphmeo  17829  qtophmeo  17841  fbun  17864  trfbas2  17867  isfil2  17880  infil  17887  trfil2  17911  filssufilg  17935  hausflim  18005  fclsnei  18043  fclsfnflim  18051  flimfnfcls  18052  ptcmplem1  18075  clssubg  18130  tgpconcomp  18134  divstgplem  18142  tsmsfbas  18149  utoptop  18256  iducn  18305  cstucnd  18306  isxmetd  18348  isxmet2d  18349  xmettpos  18371  prdsdsf  18389  prdsmet  18392  ressprdsds  18393  imasdsf1olem  18395  imasf1oxmet  18397  imasf1omet  18398  blfvalps  18405  xmetresbl  18459  metss2  18534  comet  18535  stdbdmet  18538  stdbdmopn  18540  methaus  18542  met2ndci  18544  metustfbasOLD  18587  metustfbas  18588  nrmmetd  18614  subgngp  18668  ngptgp  18669  sranlm  18712  nlmvscnlem1  18714  nlmvscn  18715  nrginvrcn  18719  lssnlm  18728  nghmcn  18771  qtopbaslem  18784  reconn  18851  xmetdcn2  18860  metdscn  18878  metnrm  18884  elcncf1di  18917  cncffvrn  18920  mulc1cncf  18927  cncfco  18929  reparphti  19014  tchcph  19186  ipcnlem1  19191  ipcn  19192  iscfil3  19218  bcthlem5  19273  minveclem3  19322  minveclem7  19328  ovolicc2lem4  19408  dyadmbl  19484  volcn  19490  itg1addlem1  19576  itg1addlem2  19581  itg1addlem4  19583  mbfi1fseqlem1  19599  mbfi1fseqlem3  19601  mbfi1fseqlem4  19602  mbfi1fseqlem5  19603  dvmptfsum  19851  c1liplem1  19872  dvgt0lem2  19879  ftc1a  19913  evlseu  19929  ply1domn  20038  ply1divmo  20050  fta1b  20084  ig1peu  20086  coeeu  20136  plydivalg  20208  aaliou2b  20250  ulmss  20305  ulmcn  20307  efif1olem4  20439  logccv  20546  cvxcl  20815  basellem4  20858  fsumdvdscom  20962  musum  20968  dvdsmulf1o  20971  fsumdvdsmul  20972  dchrelbasd  21015  dchrmulcl  21025  dchrinv  21037  lgsqrlem2  21118  lgsdchr  21124  lgseisenlem2  21126  lgsquadlem1  21130  lgsquadlem2  21131  dchrisumlema  21174  dchrisumlem2  21176  chpdifbndlem2  21240  pntpbnd  21274  pntibndlem3  21278  usgraedgreu  21399  usgraidx2v  21404  isgrp2d  21815  grpoinvf  21820  subgoablo  21891  ghgrplem2  21947  ghablo  21949  nvmf  22119  vacn  22182  nmcvcn  22183  smcnlem  22185  sspg  22219  ssps  22221  sspmlem  22223  0lno  22283  blocni  22298  sspph  22348  ipblnfi  22349  minvecolem7  22377  unopf1o  23411  cnvunop  23413  unoplin  23415  counop  23416  hmopadj2  23436  hmoplin  23437  bralnfn  23443  lnopeq0i  23502  hmops  23515  hmopm  23516  hmopco  23518  lnconi  23528  cnlnadjlem2  23563  adjmul  23587  adjadd  23588  cdjreui  23927  disjxpin  24020  off2  24046  xrofsup  24118  kerf1hrm  24254  pstmxmet  24284  ofcf  24478  sibfof  24646  erdszelem4  24872  erdszelem9  24877  erdsze2lem2  24882  cnpcon  24909  pconcon  24910  txpcon  24911  ptpcon  24912  cvxpcon  24921  cvxscon  24922  iccllyscon  24929  cvmseu  24955  cvmliftmo  24963  cvmlift2lem5  24986  cvmlift2lem9  24990  fprodser  25267  fprod2dlem  25296  fprodcom2  25300  brbtwn2  25836  axlowdimlem15  25887  axcontlem2  25896  axcontlem10  25904  segconeu  25937  onsuct0  26183  mblfinlem  26234  ftc1anc  26278  fnessref  26364  neibastop1  26379  filnetlem3  26400  sdclem1  26438  isbnd3  26484  prdsbnd  26493  ismtycnv  26502  ismtyhmeolem  26504  ismtyres  26508  bfplem1  26522  bfplem2  26523  bfp  26524  rrnmet  26529  ismrer1  26538  iccbnd  26540  grpokerinj  26551  isdrngo2  26565  rngogrphom  26578  rngohomco  26581  rngoisocnv  26588  iscringd  26600  erprt  26713  nacsfix  26757  rmxypairf1o  26965  wepwsolem  27107  dnnumch3  27113  fnwe2  27119  dsmmlss  27178  uvcf1  27209  frlmlbs  27217  lindff1  27258  lindfrn  27259  f1lindf  27260  mpaaeu  27323  issubmd  27351  mamucl  27424  mamudiagcl  27425  mamulid  27426  mamurid  27427  mamuass  27428  mamudi  27429  mamudir  27430  mamuvs1  27431  mamuvs2  27432  idomsubgmo  27482  mon1psubm  27493  deg1mhm  27494  dmmpt2g  27950  otsndisj  28055  otiunsndisj  28056  otiunsndisjX  28057  cshwsdisj  28248  2spotiundisj  28388  2spotmdisj  28394  lfl0f  29804  lkrlss  29830  lshpsmreu  29844  linepsubN  30486  pmapsub  30502  lautcnv  30824  lautco  30831  idltrn  30884  cdleme50f1  31277  cdleme50laut  31281  istendod  31496  dihf11  32002  dih1dimatlem  32064  lcfl7N  32236  lcfrlem9  32285  mapd1o  32383  hdmapf1oN  32603  hgmapf1oN  32641
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2702
  Copyright terms: Public domain W3C validator