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

Theorem ralrimivva 2610
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 425 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ps ) )
32ralrimivv 2609 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1621   A.wral 2518
This theorem is referenced by:  disjxiun  3994  swopo  4296  issod  4316  fcof1  5731  fliftfund  5746  soisores  5758  soisoi  5759  isocnv  5761  f1oiso  5782  caovclg  5946  caovcomg  5949  off  6027  caofrss  6044  caonncan  6049  fmpt2co  6136  poxp  6161  smo11  6349  smoiso2  6354  omsmo  6620  qsdisj2  6705  eroprf  6724  dom2lem  6869  omxpenlem  6931  xpf1o  6991  unxpdomlem3  7037  fofinf1o  7105  dffi3  7152  supmo  7171  inf3lem6  7302  cantnf  7363  rankxplim  7517  fseqenlem1  7619  fodomacn  7651  iunfictbso  7709  cofsmo  7863  infpssrlem5  7901  enfin2i  7915  fin23lem23  7920  fin23lem27  7922  fin23lem28  7934  compssiso  7968  ltordlem  9266  cju  9710  axdc4uzlem  11011  seqcaopr2  11049  seqhomo  11060  climcn2  12032  addcn2  12033  mulcn2  12035  o1of2  12052  isercolllem1  12104  fsum2dlem  12199  fsumcom2  12203  isprm6  12751  crt  12809  eulerthlem2  12813  vdwlem12  13002  imasaddfnlem  13393  imasvscafn  13402  mreexexd  13513  iscatd  13538  proplem  13555  oppccomfpropd  13593  sectmon  13643  ssctr  13665  ssceq  13666  issubc3  13686  fullsubc  13687  fullresc  13688  isfuncd  13702  idfucl  13718  cofucl  13725  funcres2b  13734  fulloppc  13759  fthoppc  13760  idffth  13770  cofull  13771  cofth  13772  ressffth  13775  setcmon  13882  setcepi  13883  resssetc  13887  resscatc  13900  catciso  13902  evlfcl  13959  uncfcurf  13976  hofcl  13996  yonedalem3  14017  yonedainv  14018  yonffthlem  14019  yoniso  14022  isdrs2  14036  isposd  14052  pospropd  14201  poslubmo  14213  mndplusf  14346  mndfo  14360  mndpropd  14361  issubmnd  14364  mhmpropd  14384  0mhm  14398  resmhm  14399  resmhm2  14400  resmhm2b  14401  mhmco  14402  submacs  14405  prdspjmhm  14406  pwsdiagmhm  14408  pwsco1mhm  14409  pwsco2mhm  14410  gsumwspan  14431  frmdsssubm  14446  frmdup1  14449  grpsubf  14508  issubg4  14601  isnsg3  14614  nsgacs  14616  0nsg  14625  nsgid  14626  isghmd  14655  ghmmhm  14656  idghm  14661  ghmnsgima  14669  ghmnsgpreima  14670  ghmf1  14674  ghmf1o  14675  gaid  14716  subgga  14717  gass  14718  gasubg  14719  lactghmga  14747  cntzsubm  14774  cntrsubgnsg  14779  odf1  14838  sylow1lem2  14873  sylow2blem2  14895  sylow3lem1  14901  lsmssv  14917  lsmidm  14936  pj1eu  14968  efglem  14988  efgtf  14994  efgred  15020  efgredeu  15024  frgpmhm  15037  frgpuptf  15042  frgpuplem  15044  mulgmhm  15090  invghm  15093  ablnsg  15102  gsum2d2lem  15187  gsum2d2  15188  gsumcom2  15189  dprd2d2  15242  ablfaclem2  15284  isrhm2d  15469  issubrg2  15528  subrgint  15530  islmodd  15596  lmodscaf  15612  lmodprop2d  15650  islssd  15656  islss4  15682  lssacs  15687  lsspropd  15737  islmhmd  15759  lmhmima  15767  lmhmpreima  15768  reslmhm  15772  lspextmo  15776  lsmcl  15799  pj1lmhm  15816  islbs2  15870  issubrngd2  15906  opprdomn  16005  abvn0b  16006  issubassa2  16047  mvrf1  16133  mplsubglem  16142  mplsubrg  16147  mplind  16206  evlslem2  16212  ply1sclf1  16327  prmirredlem  16409  expmhm  16412  expghm  16413  mulgghm2  16422  domnchr  16449  znf1o  16468  zntoslem  16473  znfld  16477  cygznlem3  16486  phlipf  16519  tgclb  16671  mretopd  16792  toponmre  16793  iscldtop  16795  ordtbaslem  16881  ordtbas2  16884  cnt0  17037  haust1  17043  cnhaus  17045  isreg2  17068  dishaus  17073  ordthaus  17075  dfcon2  17108  iuncon  17117  clscon  17119  2ndcomap  17147  dis2ndc  17149  llynlly  17166  restnlly  17171  restlly  17172  islly2  17173  llyidm  17177  nllyidm  17178  hausllycmp  17183  kgentopon  17196  txbas  17225  ptbasin2  17236  ptbasfi  17239  txcnp  17277  txcnmpt  17281  pthaus  17295  tx1stc  17307  xkococnlem  17316  xkococn  17317  cnmpt21  17328  qtoptop2  17353  qtopeu  17370  kqt0lem  17390  isr0  17391  regr1lem2  17394  kqreglem1  17395  kqreglem2  17396  kqnrmlem1  17397  kqnrmlem2  17398  nrmr0reg  17403  reghmph  17447  nrmhmph  17448  txswaphmeo  17459  qtophmeo  17471  fbun  17498  trfbas2  17501  isfil2  17514  infil  17521  trfil2  17545  filssufilg  17569  hausflim  17639  fclsnei  17677  fclsfnflim  17685  flimfnfcls  17686  ptcmplem1  17709  clssubg  17754  tgpconcomp  17758  divstgplem  17766  tsmsfbas  17773  isxmetd  17854  isxmet2d  17855  xmettpos  17876  prdsdsf  17894  prdsmet  17897  ressprdsds  17898  imasdsf1olem  17900  imasf1oxmet  17902  imasf1omet  17903  blfval  17910  xmetresbl  17946  metss2  18021  comet  18022  stdbdmet  18025  stdbdmopn  18027  methaus  18029  met2ndci  18031  nrmmetd  18060  subgngp  18114  ngptgp  18115  sranlm  18158  nlmvscnlem1  18160  nlmvscn  18161  nrginvrcn  18165  lssnlm  18174  nghmcn  18217  qtopbaslem  18230  reconn  18296  xmetdcn2  18305  metdscn  18323  metnrm  18329  elcncf1di  18362  cncffvrn  18365  mulc1cncf  18372  cncfco  18374  reparphti  18458  tchcph  18630  ipcnlem1  18635  ipcn  18636  iscfil3  18662  bcthlem5  18713  minveclem3  18756  minveclem7  18762  ovolicc2lem4  18842  dyadmbl  18918  volcn  18924  itg1addlem1  19010  itg1addlem2  19015  itg1addlem4  19017  mbfi1fseqlem1  19033  mbfi1fseqlem3  19035  mbfi1fseqlem4  19036  mbfi1fseqlem5  19037  dvmptfsum  19285  c1liplem1  19306  dvgt0lem2  19313  ftc1a  19347  evlseu  19363  ply1domn  19472  ply1divmo  19484  fta1b  19518  ig1peu  19520  coeeu  19570  plydivalg  19642  aaliou2b  19684  ulmss  19737  ulmcn  19739  efif1olem4  19870  logccv  19973  cvxcl  20242  basellem4  20284  fsumdvdscom  20388  musum  20394  dvdsmulf1o  20397  fsumdvdsmul  20398  dchrelbasd  20441  dchrmulcl  20451  dchrinv  20463  lgsqrlem2  20544  lgsdchr  20550  lgseisenlem2  20552  lgsquadlem1  20556  lgsquadlem2  20557  dchrisumlema  20600  dchrisumlem2  20602  chpdifbndlem2  20666  pntpbnd  20700  pntibndlem3  20704  isgrp2d  20863  grpoinvf  20868  subgoablo  20939  ghgrplem2  20995  ghablo  20997  nvmf  21165  vacn  21228  nmcvcn  21229  smcnlem  21231  sspg  21265  ssps  21267  sspmlem  21269  0lno  21329  blocni  21344  sspph  21394  ipblnfi  21395  minvecolem7  21423  unopf1o  22457  cnvunop  22459  unoplin  22461  counop  22462  hmopadj2  22482  hmoplin  22483  bralnfn  22489  lnopeq0i  22548  hmops  22561  hmopm  22562  hmopco  22564  lnconi  22574  cnlnadjlem2  22609  adjmul  22633  adjadd  22634  cdjreui  22973  erdszelem4  23098  erdszelem9  23103  erdsze2lem2  23108  cnpcon  23134  pconcon  23135  txpcon  23136  ptpcon  23137  cvxpcon  23146  cvxscon  23147  iccllyscon  23154  cvmseu  23180  cvmliftmo  23188  cvmlift2lem5  23211  cvmlift2lem9  23215  brbtwn2  23909  axlowdimlem15  23960  axcontlem2  23969  axcontlem10  23977  segconeu  24010  onsuct0  24256  toplat  24658  trooo  24762  rltrooo  24783  muldisc  24849  trnij  24983  sigadd  25017  fnmulcv  25052  icccon2  25068  icccon3  25069  icccon4  25070  idmon  25185  prismorcsetlemb  25281  setiscat  25347  fnessref  25661  neibastop1  25676  filnetlem3  25697  r19.21aivvaOLD  25706  sdclem1  25821  isbnd3  25876  prdsbnd  25885  ismtycnv  25894  ismtyhmeolem  25896  ismtyres  25900  bfplem1  25914  bfplem2  25915  bfp  25916  rrnmet  25921  ismrer1  25930  iccbnd  25932  grpokerinj  25943  isdrngo2  25957  rngogrphom  25970  rngohomco  25973  rngoisocnv  25980  iscringd  25992  erprt  26109  nacsfix  26155  rmxypairf1o  26364  wepwsolem  26506  dnnumch3  26512  fnwe2  26518  dsmmlss  26578  uvcf1  26609  frlmlbs  26617  lindff1  26658  lindfrn  26659  f1lindf  26660  mpaaeu  26723  issubmd  26751  mamucl  26824  mamudiagcl  26825  mamulid  26826  mamurid  26827  mamuass  26828  mamudi  26829  mamudir  26830  mamuvs1  26831  mamuvs2  26832  idomsubgmo  26882  mon1psubm  26893  deg1mhm  26894  lfl0f  28509  lkrlss  28535  lshpsmreu  28549  linepsubN  29191  pmapsub  29207  lautcnv  29529  lautco  29536  idltrn  29589  cdleme50f1  29982  cdleme50laut  29986  istendod  30201  dihf11  30707  dih1dimatlem  30769  lcfl7N  30941  lcfrlem9  30990  mapd1o  31088  hdmapf1oN  31308  hgmapf1oN  31346
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-nf 1540  df-ral 2523
  Copyright terms: Public domain W3C validator