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

Theorem ralrimivva 2637
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 2636 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 1686   A.wral 2545
This theorem is referenced by:  disjxiun  4022  swopo  4326  issod  4346  fcof1  5799  fliftfund  5814  soisores  5826  soisoi  5827  isocnv  5829  f1oiso  5850  caovclg  6014  caovcomg  6017  off  6095  caofrss  6112  caonncan  6117  fmpt2co  6204  poxp  6229  smo11  6383  smoiso2  6388  omsmo  6654  qsdisj2  6739  eroprf  6758  dom2lem  6903  omxpenlem  6965  xpf1o  7025  unxpdomlem3  7071  fofinf1o  7139  dffi3  7186  supmo  7205  inf3lem6  7336  cantnf  7397  rankxplim  7551  fseqenlem1  7653  fodomacn  7685  iunfictbso  7743  cofsmo  7897  infpssrlem5  7935  enfin2i  7949  fin23lem23  7954  fin23lem27  7956  fin23lem28  7968  compssiso  8002  ltordlem  9300  cju  9744  axdc4uzlem  11046  seqcaopr2  11084  seqhomo  11095  climcn2  12068  addcn2  12069  mulcn2  12071  o1of2  12088  isercolllem1  12140  fsum2dlem  12235  fsumcom2  12239  isprm6  12790  crt  12848  eulerthlem2  12852  vdwlem12  13041  imasaddfnlem  13432  imasvscafn  13441  mreexexd  13552  iscatd  13577  proplem  13594  oppccomfpropd  13632  sectmon  13682  ssctr  13704  ssceq  13705  issubc3  13725  fullsubc  13726  fullresc  13727  isfuncd  13741  idfucl  13757  cofucl  13764  funcres2b  13773  fulloppc  13798  fthoppc  13799  idffth  13809  cofull  13810  cofth  13811  ressffth  13814  setcmon  13921  setcepi  13922  resssetc  13926  resscatc  13939  catciso  13941  evlfcl  13998  uncfcurf  14015  hofcl  14035  yonedalem3  14056  yonedainv  14057  yonffthlem  14058  yoniso  14061  isdrs2  14075  isposd  14091  pospropd  14240  poslubmo  14252  mndplusf  14385  mndfo  14399  mndpropd  14400  issubmnd  14403  mhmpropd  14423  0mhm  14437  resmhm  14438  resmhm2  14439  resmhm2b  14440  mhmco  14441  submacs  14444  prdspjmhm  14445  pwsdiagmhm  14447  pwsco1mhm  14448  pwsco2mhm  14449  gsumwspan  14470  frmdsssubm  14485  frmdup1  14488  grpsubf  14547  issubg4  14640  isnsg3  14653  nsgacs  14655  0nsg  14664  nsgid  14665  isghmd  14694  ghmmhm  14695  idghm  14700  ghmnsgima  14708  ghmnsgpreima  14709  ghmf1  14713  ghmf1o  14714  gaid  14755  subgga  14756  gass  14757  gasubg  14758  lactghmga  14786  cntzsubm  14813  cntrsubgnsg  14818  odf1  14877  sylow1lem2  14912  sylow2blem2  14934  sylow3lem1  14940  lsmssv  14956  lsmidm  14975  pj1eu  15007  efglem  15027  efgtf  15033  efgred  15059  efgredeu  15063  frgpmhm  15076  frgpuptf  15081  frgpuplem  15083  mulgmhm  15129  invghm  15132  ablnsg  15141  gsum2d2lem  15226  gsum2d2  15227  gsumcom2  15228  dprd2d2  15281  ablfaclem2  15323  isrhm2d  15508  issubrg2  15567  subrgint  15569  islmodd  15635  lmodscaf  15651  lmodprop2d  15689  islssd  15695  islss4  15721  lssacs  15726  lsspropd  15776  islmhmd  15798  lmhmima  15806  lmhmpreima  15807  reslmhm  15811  lspextmo  15815  lsmcl  15838  pj1lmhm  15855  islbs2  15909  issubrngd2  15945  opprdomn  16044  abvn0b  16045  issubassa2  16086  mvrf1  16172  mplsubglem  16181  mplsubrg  16186  mplind  16245  evlslem2  16251  ply1sclf1  16366  prmirredlem  16448  expmhm  16451  expghm  16452  mulgghm2  16461  domnchr  16488  znf1o  16507  zntoslem  16512  znfld  16516  cygznlem3  16525  phlipf  16558  tgclb  16710  mretopd  16831  toponmre  16832  iscldtop  16834  ordtbaslem  16920  ordtbas2  16923  cnt0  17076  haust1  17082  cnhaus  17084  isreg2  17107  dishaus  17112  ordthaus  17114  dfcon2  17147  iuncon  17156  clscon  17158  2ndcomap  17186  dis2ndc  17188  llynlly  17205  restnlly  17210  restlly  17211  islly2  17212  llyidm  17216  nllyidm  17217  hausllycmp  17222  kgentopon  17235  txbas  17264  ptbasin2  17275  ptbasfi  17278  txcnp  17316  txcnmpt  17320  pthaus  17334  tx1stc  17346  xkococnlem  17355  xkococn  17356  cnmpt21  17367  qtoptop2  17392  qtopeu  17409  kqt0lem  17429  isr0  17430  regr1lem2  17433  kqreglem1  17434  kqreglem2  17435  kqnrmlem1  17436  kqnrmlem2  17437  nrmr0reg  17442  reghmph  17486  nrmhmph  17487  txswaphmeo  17498  qtophmeo  17510  fbun  17537  trfbas2  17540  isfil2  17553  infil  17560  trfil2  17584  filssufilg  17608  hausflim  17678  fclsnei  17716  fclsfnflim  17724  flimfnfcls  17725  ptcmplem1  17748  clssubg  17793  tgpconcomp  17797  divstgplem  17805  tsmsfbas  17812  isxmetd  17893  isxmet2d  17894  xmettpos  17915  prdsdsf  17933  prdsmet  17936  ressprdsds  17937  imasdsf1olem  17939  imasf1oxmet  17941  imasf1omet  17942  blfval  17949  xmetresbl  17985  metss2  18060  comet  18061  stdbdmet  18064  stdbdmopn  18066  methaus  18068  met2ndci  18070  nrmmetd  18099  subgngp  18153  ngptgp  18154  sranlm  18197  nlmvscnlem1  18199  nlmvscn  18200  nrginvrcn  18204  lssnlm  18213  nghmcn  18256  qtopbaslem  18269  reconn  18335  xmetdcn2  18344  metdscn  18362  metnrm  18368  elcncf1di  18401  cncffvrn  18404  mulc1cncf  18411  cncfco  18413  reparphti  18497  tchcph  18669  ipcnlem1  18674  ipcn  18675  iscfil3  18701  bcthlem5  18752  minveclem3  18795  minveclem7  18801  ovolicc2lem4  18881  dyadmbl  18957  volcn  18963  itg1addlem1  19049  itg1addlem2  19054  itg1addlem4  19056  mbfi1fseqlem1  19072  mbfi1fseqlem3  19074  mbfi1fseqlem4  19075  mbfi1fseqlem5  19076  dvmptfsum  19324  c1liplem1  19345  dvgt0lem2  19352  ftc1a  19386  evlseu  19402  ply1domn  19511  ply1divmo  19523  fta1b  19557  ig1peu  19559  coeeu  19609  plydivalg  19681  aaliou2b  19723  ulmss  19776  ulmcn  19778  efif1olem4  19909  logccv  20012  cvxcl  20281  basellem4  20323  fsumdvdscom  20427  musum  20433  dvdsmulf1o  20436  fsumdvdsmul  20437  dchrelbasd  20480  dchrmulcl  20490  dchrinv  20502  lgsqrlem2  20583  lgsdchr  20589  lgseisenlem2  20591  lgsquadlem1  20595  lgsquadlem2  20596  dchrisumlema  20639  dchrisumlem2  20641  chpdifbndlem2  20705  pntpbnd  20739  pntibndlem3  20743  isgrp2d  20904  grpoinvf  20909  subgoablo  20980  ghgrplem2  21036  ghablo  21038  nvmf  21206  vacn  21269  nmcvcn  21270  smcnlem  21272  sspg  21306  ssps  21308  sspmlem  21310  0lno  21370  blocni  21385  sspph  21435  ipblnfi  21436  minvecolem7  21464  unopf1o  22498  cnvunop  22500  unoplin  22502  counop  22503  hmopadj2  22523  hmoplin  22524  bralnfn  22530  lnopeq0i  22589  hmops  22602  hmopm  22603  hmopco  22605  lnconi  22615  cnlnadjlem2  22650  adjmul  22674  adjadd  22675  cdjreui  23014  off2  23210  xrofsup  23257  ofcf  23466  erdszelem4  23727  erdszelem9  23732  erdsze2lem2  23737  cnpcon  23763  pconcon  23764  txpcon  23765  ptpcon  23766  cvxpcon  23775  cvxscon  23776  iccllyscon  23783  cvmseu  23809  cvmliftmo  23817  cvmlift2lem5  23840  cvmlift2lem9  23844  brbtwn2  24535  axlowdimlem15  24586  axcontlem2  24595  axcontlem10  24603  segconeu  24636  onsuct0  24882  toplat  25301  trooo  25405  rltrooo  25426  muldisc  25492  trnij  25626  sigadd  25660  fnmulcv  25695  icccon2  25711  icccon3  25712  icccon4  25713  idmon  25828  prismorcsetlemb  25924  setiscat  25990  fnessref  26304  neibastop1  26319  filnetlem3  26340  r19.21aivvaOLD  26349  sdclem1  26464  isbnd3  26519  prdsbnd  26528  ismtycnv  26537  ismtyhmeolem  26539  ismtyres  26543  bfplem1  26557  bfplem2  26558  bfp  26559  rrnmet  26564  ismrer1  26573  iccbnd  26575  grpokerinj  26586  isdrngo2  26600  rngogrphom  26613  rngohomco  26616  rngoisocnv  26623  iscringd  26635  erprt  26752  nacsfix  26798  rmxypairf1o  27007  wepwsolem  27149  dnnumch3  27155  fnwe2  27161  dsmmlss  27221  uvcf1  27252  frlmlbs  27260  lindff1  27301  lindfrn  27302  f1lindf  27303  mpaaeu  27366  issubmd  27394  mamucl  27467  mamudiagcl  27468  mamulid  27469  mamurid  27470  mamuass  27471  mamudi  27472  mamudir  27473  mamuvs1  27474  mamuvs2  27475  idomsubgmo  27525  mon1psubm  27536  deg1mhm  27537  dmmpt2g  27992  lfl0f  29332  lkrlss  29358  lshpsmreu  29372  linepsubN  30014  pmapsub  30030  lautcnv  30352  lautco  30359  idltrn  30412  cdleme50f1  30805  cdleme50laut  30809  istendod  31024  dihf11  31530  dih1dimatlem  31592  lcfl7N  31764  lcfrlem9  31813  mapd1o  31911  hdmapf1oN  32131  hgmapf1oN  32169
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-11 1717
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1534  df-ral 2550
  Copyright terms: Public domain W3C validator