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

Theorem ralrimivva 2803
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 2802 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 1756   A.wral 2710
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2715
This theorem is referenced by:  disjxiun  4284  swopo  4646  issod  4666  fcof1  5986  fliftfund  6001  soisores  6013  soisoi  6014  isocnv  6016  f1oiso  6037  caovclg  6250  caovcomg  6253  off  6329  caofrss  6348  caonncan  6353  dmmpt2g  6641  fnmpt2ovd  6646  fmpt2co  6651  poxp  6679  smo11  6817  smoiso2  6822  omsmo  7085  qsdisj2  7170  eroprf  7190  dom2lem  7341  omxpenlem  7404  xpf1o  7465  unxpdomlem3  7511  fofinf1o  7584  dffi3  7673  supmo  7694  inf3lem6  7831  cantnf  7893  cantnfOLD  7915  rankxplim  8078  fseqenlem1  8186  fodomacn  8218  iunfictbso  8276  cofsmo  8430  infpssrlem5  8468  enfin2i  8482  fin23lem23  8487  fin23lem27  8489  fin23lem28  8501  compssiso  8535  ltordlem  9857  cju  10310  axdc4uzlem  11796  seqcaopr2  11834  seqhomo  11845  wrd2ind  12364  climcn2  13062  addcn2  13063  mulcn2  13065  o1of2  13082  isercolllem1  13134  fsum2dlem  13229  fsumcom2  13233  isprm6  13787  crt  13845  eulerthlem2  13849  vdwlem12  14045  cshwsdisj  14117  imasaddfnlem  14458  imasvscafn  14467  mreexexd  14578  iscatd  14603  proplem  14620  oppccomfpropd  14658  sectmon  14708  ssctr  14730  ssceq  14731  issubc3  14751  fullsubc  14752  fullresc  14753  isfuncd  14767  idfucl  14783  cofucl  14790  funcres2b  14799  fulloppc  14824  fthoppc  14825  idffth  14835  cofull  14836  cofth  14837  ressffth  14840  setcmon  14947  setcepi  14948  resssetc  14952  resscatc  14965  catciso  14967  evlfcl  15024  uncfcurf  15041  hofcl  15061  yonedalem3  15082  yonedainv  15083  yonffthlem  15084  yoniso  15087  isdrs2  15101  isposd  15117  pospropd  15296  poslubmo  15308  posglbmo  15309  mndplusf  15423  mndfo  15437  mndpropd  15438  issubmnd  15441  mhmpropd  15462  issubmd  15468  0mhm  15477  resmhm  15478  resmhm2  15479  resmhm2b  15480  mhmco  15481  submacs  15484  prdspjmhm  15486  pwsdiagmhm  15488  pwsco1mhm  15489  pwsco2mhm  15490  gsumwspan  15515  frmdsssubm  15530  frmdup1  15533  grpsubf  15596  issubg4  15691  grpissubg  15692  isnsg3  15706  nsgacs  15708  0nsg  15717  nsgid  15718  isghmd  15747  ghmmhm  15748  idghm  15753  ghmnsgima  15761  ghmnsgpreima  15762  ghmf1  15766  ghmf1o  15767  gaid  15808  subgga  15809  gass  15810  gasubg  15811  cntzsubm  15844  cntrsubgnsg  15849  lactghmga  15900  odf1  16054  sylow1lem2  16089  sylow2blem2  16111  sylow3lem1  16117  lsmssv  16133  lsmidm  16152  pj1eu  16184  efglem  16204  efgtf  16210  efgred  16236  efgredeu  16240  frgpmhm  16253  frgpuptf  16258  frgpuplem  16260  mulgmhm  16306  invghm  16309  ablnsg  16320  gsum2d2lem  16453  gsum2d2  16454  gsumcom2  16455  dprd2d2  16531  ablfaclem2  16575  srglmhm  16622  srgrmhm  16623  isrhm2d  16804  issubrg2  16863  subrgint  16865  islmodd  16932  lmodscaf  16948  lmodprop2d  16985  islssd  16994  islss4  17020  lssacs  17025  lsspropd  17075  islmhmd  17097  lmhmima  17105  lmhmpreima  17106  reslmhm  17110  lspextmo  17114  lsmcl  17141  pj1lmhm  17158  islbs2  17212  issubrngd2  17247  opprdomn  17350  abvn0b  17351  issubassa2  17392  mvrf1  17475  mplsubglem  17487  mplsubglemOLD  17489  mplsubrg  17496  mplind  17559  evlslem2  17572  evlseu  17577  ply1sclf1  17716  expmhm  17855  nn0srg  17856  prmirredlem  17892  prmirredlemOLD  17895  expghm  17898  expghmOLD  17899  mulgghm2  17900  mulgghm2OLD  17903  domnchr  17938  znf1o  17959  zntoslem  17964  znfld  17968  cygznlem3  17977  phlipf  18056  dsmmlss  18144  uvcf1  18192  frlmlbs  18200  lindff1  18224  lindfrn  18225  f1lindf  18226  mamucl  18276  mamudiagcl  18277  mamulid  18279  mamurid  18280  mamuass  18281  mamudi  18282  mamudir  18283  mamuvs1  18284  mamuvs2  18285  matbas2d  18299  mavmul0g  18339  mdetunilem9  18401  mdetuni0  18402  mdetmul  18404  madutpos  18423  smadiadetlem4  18450  tgclb  18550  mretopd  18671  toponmre  18672  iscldtop  18674  ordtbaslem  18767  ordtbas2  18770  cnt0  18925  haust1  18931  cnhaus  18933  isreg2  18956  dishaus  18961  ordthaus  18963  dfcon2  18998  iuncon  19007  clscon  19009  2ndcomap  19037  dis2ndc  19039  llynlly  19056  restnlly  19061  restlly  19062  islly2  19063  llyidm  19067  nllyidm  19068  hausllycmp  19073  kgentopon  19086  txbas  19115  ptbasin2  19126  ptbasfi  19129  txcnp  19168  txcnmpt  19172  pthaus  19186  tx1stc  19198  xkococnlem  19207  xkococn  19208  cnmpt21  19219  qtoptop2  19247  qtopeu  19264  kqt0lem  19284  isr0  19285  regr1lem2  19288  kqreglem1  19289  kqreglem2  19290  kqnrmlem1  19291  kqnrmlem2  19292  nrmr0reg  19297  reghmph  19341  nrmhmph  19342  txswaphmeo  19353  qtophmeo  19365  fbun  19388  trfbas2  19391  isfil2  19404  infil  19411  trfil2  19435  filssufilg  19459  hausflim  19529  fclsnei  19567  fclsfnflim  19575  flimfnfcls  19576  ptcmplem1  19599  clssubg  19654  tgpconcomp  19658  divstgplem  19666  tsmsfbas  19673  utoptop  19784  iducn  19833  cstucnd  19834  isxmetd  19876  isxmet2d  19877  xmettpos  19899  prdsdsf  19917  prdsmet  19920  ressprdsds  19921  imasdsf1olem  19923  imasf1oxmet  19925  imasf1omet  19926  blfvalps  19933  xmetresbl  19987  metss2  20062  comet  20063  stdbdmet  20066  stdbdmopn  20068  methaus  20070  met2ndci  20072  metustfbasOLD  20115  metustfbas  20116  nrmmetd  20142  subgngp  20196  ngptgp  20197  sranlm  20240  nlmvscnlem1  20242  nlmvscn  20243  nrginvrcn  20247  lssnlm  20256  nghmcn  20299  qtopbaslem  20312  reconn  20380  xmetdcn2  20389  metdscn  20407  metnrm  20413  elcncf1di  20446  cncffvrn  20449  mulc1cncf  20456  cncfco  20458  reparphti  20544  tchcph  20727  ipcnlem1  20732  ipcn  20733  iscfil3  20759  bcthlem5  20814  rrxmet  20882  minveclem3  20891  minveclem7  20897  ovolicc2lem4  20978  dyadmbl  21055  volcn  21061  itg1addlem1  21145  itg1addlem2  21150  itg1addlem4  21152  mbfi1fseqlem1  21168  mbfi1fseqlem3  21170  mbfi1fseqlem4  21171  mbfi1fseqlem5  21172  dvmptfsum  21422  c1liplem1  21443  dvgt0lem2  21450  ftc1a  21484  ply1domn  21570  ply1divmo  21582  fta1b  21616  ig1peu  21618  coeeu  21668  plydivalg  21740  aaliou2b  21782  ulmss  21837  ulmcn  21839  efif1olem4  21976  logccv  22083  cvxcl  22353  basellem4  22396  fsumdvdscom  22500  musum  22506  dvdsmulf1o  22509  fsumdvdsmul  22510  dchrelbasd  22553  dchrmulcl  22563  dchrinv  22575  lgsqrlem2  22656  lgsdchr  22662  lgseisenlem2  22664  lgsquadlem1  22668  lgsquadlem2  22669  dchrisumlema  22712  dchrisumlem2  22714  chpdifbndlem2  22778  pntpbnd  22812  pntibndlem3  22816  axtgcont  22905  ercgrg  22944  tgisline  23005  tghilbert1_2  23014  mirreu3  23026  f1otrgds  23066  f1otrg  23068  f1otrge  23069  xmstrkgc  23083  brbtwn2  23102  axlowdimlem15  23153  axcontlem2  23162  axcontlem10  23170  eengtrkg  23182  eengtrkge  23183  usgraedgreu  23257  usgraidx2v  23262  isgrp2d  23673  grpoinvf  23678  subgoablo  23749  ghgrplem2  23805  ghablo  23807  nvmf  23977  vacn  24040  nmcvcn  24041  smcnlem  24043  sspg  24077  ssps  24079  sspmlem  24081  0lno  24141  blocni  24156  sspph  24206  ipblnfi  24207  minvecolem7  24235  unopf1o  25271  cnvunop  25273  unoplin  25275  counop  25276  hmopadj2  25296  hmoplin  25297  bralnfn  25303  lnopeq0i  25362  hmops  25375  hmopm  25376  hmopco  25378  lnconi  25388  cnlnadjlem2  25423  adjmul  25447  adjadd  25448  cdjreui  25787  disjxpin  25881  off2  25910  f1od2  25975  xrofsup  26006  odutos  26075  abliso  26110  archiabllem1  26161  archiabllem2  26165  suborng  26234  kerf1hrm  26243  xrge0slmod  26264  pstmxmet  26276  ofcf  26497  sibfof  26678  erdszelem4  27034  erdszelem9  27039  erdsze2lem2  27044  cnpcon  27071  pconcon  27072  txpcon  27073  ptpcon  27074  cvxpcon  27083  cvxscon  27084  iccllyscon  27091  cvmseu  27117  cvmliftmo  27125  cvmlift2lem5  27148  cvmlift2lem9  27152  fprodser  27413  fprod2dlem  27442  fprodcom2  27446  segconeu  27993  onsuct0  28239  fin2so  28369  heicant  28379  mblfinlem2  28382  ftc1anc  28428  fnessref  28518  neibastop1  28533  filnetlem3  28554  sdclem1  28592  isbnd3  28636  prdsbnd  28645  ismtycnv  28654  ismtyhmeolem  28656  ismtyres  28660  bfplem1  28674  bfplem2  28675  bfp  28676  rrnmet  28681  ismrer1  28690  iccbnd  28692  grpokerinj  28703  isdrngo2  28717  rngogrphom  28730  rngohomco  28733  rngoisocnv  28740  iscringd  28752  erprt  28971  nacsfix  29001  rmxypairf1o  29205  wepwsolem  29347  dnnumch3  29353  fnwe2  29359  mpaaeu  29460  idomsubgmo  29516  mon1psubm  29527  deg1mhm  29528  otsndisj  30084  otiunsndisj  30085  otiunsndisjX  30086  wlknwwlkninj  30296  wlkiswwlkinj  30303  wwlkextinj  30315  clwwlkf1  30411  2spotiundisj  30608  2spotmdisj  30614  numclwlk1lem2f1  30640  dmatid  30797  dmatsubcl  30800  dmatsgrp  30801  dmatmulcl  30802  dmatsrng  30803  dmatcrng  30804  scmatsgrp  30808  scmatsrng  30810  scmatcrng  30811  scmatsgrp1  30812  scmatsrng1  30813  pmatcollpw1  30819  lindslinindsimp1  30880  lmod1  30923  lfl0f  32554  lkrlss  32580  lshpsmreu  32594  linepsubN  33236  pmapsub  33252  lautcnv  33574  lautco  33581  idltrn  33634  cdleme50f1  34027  cdleme50laut  34031  istendod  34246  dihf11  34752  dih1dimatlem  34814  lcfl7N  34986  lcfrlem9  35035  mapd1o  35133  hdmapf1oN  35353  hgmapf1oN  35391
  Copyright terms: Public domain W3C validator