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

Theorem ralrimivva 2798
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 434 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ps ) )
32ralrimivv 2797 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1755   A.wral 2705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710
This theorem is referenced by:  disjxiun  4277  swopo  4638  issod  4658  fcof1  5978  fliftfund  5993  soisores  6005  soisoi  6006  isocnv  6008  f1oiso  6029  caovclg  6244  caovcomg  6247  off  6323  caofrss  6342  caonncan  6347  dmmpt2g  6635  fnmpt2ovd  6640  fmpt2co  6645  poxp  6673  smo11  6811  smoiso2  6816  omsmo  7081  qsdisj2  7166  eroprf  7186  dom2lem  7337  omxpenlem  7400  xpf1o  7461  unxpdomlem3  7507  fofinf1o  7580  dffi3  7669  supmo  7690  inf3lem6  7827  cantnf  7889  cantnfOLD  7911  rankxplim  8074  fseqenlem1  8182  fodomacn  8214  iunfictbso  8272  cofsmo  8426  infpssrlem5  8464  enfin2i  8478  fin23lem23  8483  fin23lem27  8485  fin23lem28  8497  compssiso  8531  ltordlem  9853  cju  10306  axdc4uzlem  11788  seqcaopr2  11826  seqhomo  11837  wrd2ind  12356  climcn2  13054  addcn2  13055  mulcn2  13057  o1of2  13074  isercolllem1  13126  fsum2dlem  13221  fsumcom2  13225  isprm6  13778  crt  13836  eulerthlem2  13840  vdwlem12  14036  cshwsdisj  14108  imasaddfnlem  14449  imasvscafn  14458  mreexexd  14569  iscatd  14594  proplem  14611  oppccomfpropd  14649  sectmon  14699  ssctr  14721  ssceq  14722  issubc3  14742  fullsubc  14743  fullresc  14744  isfuncd  14758  idfucl  14774  cofucl  14781  funcres2b  14790  fulloppc  14815  fthoppc  14816  idffth  14826  cofull  14827  cofth  14828  ressffth  14831  setcmon  14938  setcepi  14939  resssetc  14943  resscatc  14956  catciso  14958  evlfcl  15015  uncfcurf  15032  hofcl  15052  yonedalem3  15073  yonedainv  15074  yonffthlem  15075  yoniso  15078  isdrs2  15092  isposd  15108  pospropd  15287  poslubmo  15299  posglbmo  15300  mndplusf  15414  mndfo  15428  mndpropd  15429  issubmnd  15432  mhmpropd  15453  issubmd  15459  0mhm  15468  resmhm  15469  resmhm2  15470  resmhm2b  15471  mhmco  15472  submacs  15475  prdspjmhm  15477  pwsdiagmhm  15479  pwsco1mhm  15480  pwsco2mhm  15481  gsumwspan  15504  frmdsssubm  15519  frmdup1  15522  grpsubf  15585  issubg4  15680  grpissubg  15681  isnsg3  15695  nsgacs  15697  0nsg  15706  nsgid  15707  isghmd  15736  ghmmhm  15737  idghm  15742  ghmnsgima  15750  ghmnsgpreima  15751  ghmf1  15755  ghmf1o  15756  gaid  15797  subgga  15798  gass  15799  gasubg  15800  cntzsubm  15833  cntrsubgnsg  15838  lactghmga  15889  odf1  16043  sylow1lem2  16078  sylow2blem2  16100  sylow3lem1  16106  lsmssv  16122  lsmidm  16141  pj1eu  16173  efglem  16193  efgtf  16199  efgred  16225  efgredeu  16229  frgpmhm  16242  frgpuptf  16247  frgpuplem  16249  mulgmhm  16295  invghm  16298  ablnsg  16309  gsum2d2lem  16439  gsum2d2  16440  gsumcom2  16441  dprd2d2  16517  ablfaclem2  16561  isrhm2d  16750  issubrg2  16809  subrgint  16811  islmodd  16878  lmodscaf  16894  lmodprop2d  16931  islssd  16939  islss4  16965  lssacs  16970  lsspropd  17020  islmhmd  17042  lmhmima  17050  lmhmpreima  17051  reslmhm  17055  lspextmo  17059  lsmcl  17086  pj1lmhm  17103  islbs2  17157  issubrngd2  17192  opprdomn  17295  abvn0b  17296  issubassa2  17337  mvrf1  17432  mplsubglem  17444  mplsubglemOLD  17446  mplsubrg  17453  mplind  17516  evlslem2  17525  ply1sclf1  17639  expmhm  17724  prmirredlem  17759  prmirredlemOLD  17762  expghm  17765  expghmOLD  17766  mulgghm2  17767  mulgghm2OLD  17770  domnchr  17805  znf1o  17826  zntoslem  17831  znfld  17835  cygznlem3  17844  phlipf  17923  dsmmlss  18011  uvcf1  18059  frlmlbs  18067  lindff1  18091  lindfrn  18092  f1lindf  18093  mamucl  18143  mamudiagcl  18144  mamulid  18146  mamurid  18147  mamuass  18148  mamudi  18149  mamudir  18150  mamuvs1  18151  mamuvs2  18152  matbas2d  18166  mavmul0g  18206  mdetunilem9  18268  mdetuni0  18269  mdetmul  18271  madutpos  18290  smadiadetlem4  18317  tgclb  18417  mretopd  18538  toponmre  18539  iscldtop  18541  ordtbaslem  18634  ordtbas2  18637  cnt0  18792  haust1  18798  cnhaus  18800  isreg2  18823  dishaus  18828  ordthaus  18830  dfcon2  18865  iuncon  18874  clscon  18876  2ndcomap  18904  dis2ndc  18906  llynlly  18923  restnlly  18928  restlly  18929  islly2  18930  llyidm  18934  nllyidm  18935  hausllycmp  18940  kgentopon  18953  txbas  18982  ptbasin2  18993  ptbasfi  18996  txcnp  19035  txcnmpt  19039  pthaus  19053  tx1stc  19065  xkococnlem  19074  xkococn  19075  cnmpt21  19086  qtoptop2  19114  qtopeu  19131  kqt0lem  19151  isr0  19152  regr1lem2  19155  kqreglem1  19156  kqreglem2  19157  kqnrmlem1  19158  kqnrmlem2  19159  nrmr0reg  19164  reghmph  19208  nrmhmph  19209  txswaphmeo  19220  qtophmeo  19232  fbun  19255  trfbas2  19258  isfil2  19271  infil  19278  trfil2  19302  filssufilg  19326  hausflim  19396  fclsnei  19434  fclsfnflim  19442  flimfnfcls  19443  ptcmplem1  19466  clssubg  19521  tgpconcomp  19525  divstgplem  19533  tsmsfbas  19540  utoptop  19651  iducn  19700  cstucnd  19701  isxmetd  19743  isxmet2d  19744  xmettpos  19766  prdsdsf  19784  prdsmet  19787  ressprdsds  19788  imasdsf1olem  19790  imasf1oxmet  19792  imasf1omet  19793  blfvalps  19800  xmetresbl  19854  metss2  19929  comet  19930  stdbdmet  19933  stdbdmopn  19935  methaus  19937  met2ndci  19939  metustfbasOLD  19982  metustfbas  19983  nrmmetd  20009  subgngp  20063  ngptgp  20064  sranlm  20107  nlmvscnlem1  20109  nlmvscn  20110  nrginvrcn  20114  lssnlm  20123  nghmcn  20166  qtopbaslem  20179  reconn  20247  xmetdcn2  20256  metdscn  20274  metnrm  20280  elcncf1di  20313  cncffvrn  20316  mulc1cncf  20323  cncfco  20325  reparphti  20411  tchcph  20594  ipcnlem1  20599  ipcn  20600  iscfil3  20626  bcthlem5  20681  rrxmet  20749  minveclem3  20758  minveclem7  20764  ovolicc2lem4  20845  dyadmbl  20922  volcn  20928  itg1addlem1  21012  itg1addlem2  21017  itg1addlem4  21019  mbfi1fseqlem1  21035  mbfi1fseqlem3  21037  mbfi1fseqlem4  21038  mbfi1fseqlem5  21039  dvmptfsum  21289  c1liplem1  21310  dvgt0lem2  21317  ftc1a  21351  evlseu  21368  ply1domn  21480  ply1divmo  21492  fta1b  21526  ig1peu  21528  coeeu  21578  plydivalg  21650  aaliou2b  21692  ulmss  21747  ulmcn  21749  efif1olem4  21886  logccv  21993  cvxcl  22263  basellem4  22306  fsumdvdscom  22410  musum  22416  dvdsmulf1o  22419  fsumdvdsmul  22420  dchrelbasd  22463  dchrmulcl  22473  dchrinv  22485  lgsqrlem2  22566  lgsdchr  22572  lgseisenlem2  22574  lgsquadlem1  22578  lgsquadlem2  22579  dchrisumlema  22622  dchrisumlem2  22624  chpdifbndlem2  22688  pntpbnd  22722  pntibndlem3  22726  axtgcont  22815  ercgrg  22850  tgisline  22906  tghilbert1_2  22915  mirreu3  22924  f1otrgds  22938  f1otrg  22940  f1otrge  22941  xmstrkgc  22955  brbtwn2  22974  axlowdimlem15  23025  axcontlem2  23034  axcontlem10  23042  eengtrkg  23054  eengtrkge  23055  usgraedgreu  23129  usgraidx2v  23134  isgrp2d  23545  grpoinvf  23550  subgoablo  23621  ghgrplem2  23677  ghablo  23679  nvmf  23849  vacn  23912  nmcvcn  23913  smcnlem  23915  sspg  23949  ssps  23951  sspmlem  23953  0lno  24013  blocni  24028  sspph  24078  ipblnfi  24079  minvecolem7  24107  unopf1o  25143  cnvunop  25145  unoplin  25147  counop  25148  hmopadj2  25168  hmoplin  25169  bralnfn  25175  lnopeq0i  25234  hmops  25247  hmopm  25248  hmopco  25250  lnconi  25260  cnlnadjlem2  25295  adjmul  25319  adjadd  25320  cdjreui  25659  disjxpin  25754  off2  25783  f1od2  25848  xrofsup  25878  odutos  25947  abliso  25983  archiabllem1  26034  archiabllem2  26038  nn0srg  26063  suborng  26136  kerf1hrm  26145  xrge0slmod  26166  pstmxmet  26178  ofcf  26399  sibfof  26574  erdszelem4  26930  erdszelem9  26935  erdsze2lem2  26940  cnpcon  26967  pconcon  26968  txpcon  26969  ptpcon  26970  cvxpcon  26979  cvxscon  26980  iccllyscon  26987  cvmseu  27013  cvmliftmo  27021  cvmlift2lem5  27044  cvmlift2lem9  27048  fprodser  27309  fprod2dlem  27338  fprodcom2  27342  segconeu  27889  onsuct0  28135  fin2so  28260  heicant  28270  mblfinlem2  28273  ftc1anc  28319  fnessref  28409  neibastop1  28424  filnetlem3  28445  sdclem1  28483  isbnd3  28527  prdsbnd  28536  ismtycnv  28545  ismtyhmeolem  28547  ismtyres  28551  bfplem1  28565  bfplem2  28566  bfp  28567  rrnmet  28572  ismrer1  28581  iccbnd  28583  grpokerinj  28594  isdrngo2  28608  rngogrphom  28621  rngohomco  28624  rngoisocnv  28631  iscringd  28643  erprt  28863  nacsfix  28893  rmxypairf1o  29097  wepwsolem  29239  dnnumch3  29245  fnwe2  29251  mpaaeu  29352  idomsubgmo  29408  mon1psubm  29419  deg1mhm  29420  otsndisj  29977  otiunsndisj  29978  otiunsndisjX  29979  wlknwwlkninj  30189  wlkiswwlkinj  30196  wwlkextinj  30208  clwwlkf1  30304  2spotiundisj  30501  2spotmdisj  30507  numclwlk1lem2f1  30533  lindslinindsimp1  30700  lmod1  30743  lfl0f  32287  lkrlss  32313  lshpsmreu  32327  linepsubN  32969  pmapsub  32985  lautcnv  33307  lautco  33314  idltrn  33367  cdleme50f1  33760  cdleme50laut  33764  istendod  33979  dihf11  34485  dih1dimatlem  34547  lcfl7N  34719  lcfrlem9  34768  mapd1o  34866  hdmapf1oN  35086  hgmapf1oN  35124
  Copyright terms: Public domain W3C validator