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

Theorem ralrimivva 2597
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 2596 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 2509
This theorem is referenced by:  disjxiun  3917  swopo  4217  issod  4237  fcof1  5649  fliftfund  5664  soisores  5676  soisoi  5677  isocnv  5679  f1oiso  5700  caovclg  5864  caovcomg  5867  off  5945  caofrss  5962  caonncan  5967  fmpt2co  6054  poxp  6079  smo11  6267  smoiso2  6272  omsmo  6538  qsdisj2  6623  eroprf  6642  dom2lem  6787  omxpenlem  6848  xpf1o  6908  unxpdomlem3  6954  fofinf1o  7022  dffi3  7068  inf3lem6  7218  cantnf  7279  rankxplim  7433  fseqenlem1  7535  fodomacn  7567  iunfictbso  7625  cofsmo  7779  infpssrlem5  7817  enfin2i  7831  fin23lem23  7836  fin23lem27  7838  fin23lem28  7850  compssiso  7884  ltordlem  9178  cju  9622  axdc4uzlem  10922  seqcaopr2  10960  seqhomo  10971  climcn2  11943  addcn2  11944  mulcn2  11946  o1of2  11963  isercolllem1  12015  fsum2dlem  12110  fsumcom2  12114  isprm6  12662  crt  12720  eulerthlem2  12724  vdwlem12  12913  imasaddfnlem  13304  imasvscafn  13313  iscatd  13419  proplem  13436  oppccomfpropd  13474  sectmon  13524  ssctr  13546  ssceq  13547  issubc3  13567  fullsubc  13568  fullresc  13569  isfuncd  13583  idfucl  13599  cofucl  13606  funcres2b  13615  fulloppc  13640  fthoppc  13641  idffth  13651  cofull  13652  cofth  13653  ressffth  13656  setcmon  13763  setcepi  13764  resssetc  13768  resscatc  13781  catciso  13783  evlfcl  13840  uncfcurf  13857  hofcl  13877  yonedalem3  13898  yonedainv  13899  yonffthlem  13900  yoniso  13903  isdrs2  13917  isposd  13933  pospropd  14082  poslubmo  14094  mndplusf  14218  mndfo  14232  mndpropd  14233  issubmnd  14236  mhmpropd  14256  0mhm  14270  resmhm  14271  resmhm2  14272  resmhm2b  14273  mhmco  14274  submacs  14277  prdspjmhm  14278  pwsdiagmhm  14280  pwsco1mhm  14281  pwsco2mhm  14282  gsumwspan  14303  frmdsssubm  14318  frmdup1  14321  grpsubf  14380  issubg4  14473  isnsg3  14486  nsgacs  14488  0nsg  14497  nsgid  14498  isghmd  14527  ghmmhm  14528  idghm  14533  ghmnsgima  14541  ghmnsgpreima  14542  ghmf1  14546  ghmf1o  14547  gaid  14588  subgga  14589  gass  14590  gasubg  14591  lactghmga  14619  cntzsubm  14646  cntrsubgnsg  14651  odf1  14710  sylow1lem2  14745  sylow2blem2  14767  sylow3lem1  14773  lsmssv  14789  lsmidm  14808  pj1eu  14840  efglem  14860  efgtf  14866  efgred  14892  efgredeu  14896  frgpmhm  14909  frgpuptf  14914  frgpuplem  14916  mulgmhm  14962  invghm  14965  ablnsg  14974  gsum2d2lem  15059  gsum2d2  15060  gsumcom2  15061  dprd2d2  15114  ablfaclem2  15156  isrhm2d  15341  issubrg2  15400  subrgint  15402  islmodd  15468  lmodscaf  15484  lmodprop2d  15522  islssd  15528  islss4  15554  lssacs  15559  lsspropd  15609  islmhmd  15631  lmhmima  15639  lmhmpreima  15640  reslmhm  15644  lspextmo  15648  lsmcl  15671  pj1lmhm  15688  islbs2  15741  issubrngd2  15775  opprdomn  15874  abvn0b  15875  issubassa2  15916  mvrf1  16002  mplsubglem  16011  mplsubrg  16016  mplind  16075  evlslem2  16081  ply1sclf1  16196  prmirredlem  16278  expmhm  16281  expghm  16282  mulgghm2  16291  domnchr  16318  znf1o  16337  zntoslem  16342  znfld  16346  cygznlem3  16355  phlipf  16388  tgclb  16540  mretopd  16661  toponmre  16662  iscldtop  16664  ordtbaslem  16750  ordtbas2  16753  cnt0  16906  haust1  16912  cnhaus  16914  isreg2  16937  dishaus  16942  ordthaus  16944  dfcon2  16977  iuncon  16986  clscon  16988  2ndcomap  17016  dis2ndc  17018  llynlly  17035  restnlly  17040  restlly  17041  islly2  17042  llyidm  17046  nllyidm  17047  hausllycmp  17052  kgentopon  17065  txbas  17094  ptbasin2  17105  ptbasfi  17108  txcnp  17146  txcnmpt  17150  pthaus  17164  tx1stc  17176  xkococnlem  17185  xkococn  17186  cnmpt21  17197  qtoptop2  17222  qtopeu  17239  kqt0lem  17259  isr0  17260  regr1lem2  17263  kqreglem1  17264  kqreglem2  17265  kqnrmlem1  17266  kqnrmlem2  17267  nrmr0reg  17272  reghmph  17316  nrmhmph  17317  txswaphmeo  17328  qtophmeo  17340  fbun  17367  trfbas2  17370  isfil2  17383  infil  17390  trfil2  17414  filssufilg  17438  hausflim  17508  fclsnei  17546  fclsfnflim  17554  flimfnfcls  17555  ptcmplem1  17578  clssubg  17623  tgpconcomp  17627  divstgplem  17635  tsmsfbas  17642  isxmetd  17723  isxmet2d  17724  xmettpos  17745  prdsdsf  17763  prdsmet  17766  ressprdsds  17767  imasdsf1olem  17769  imasf1oxmet  17771  imasf1omet  17772  blfval  17779  xmetresbl  17815  metss2  17890  comet  17891  stdbdmet  17894  stdbdmopn  17896  methaus  17898  met2ndci  17900  nrmmetd  17929  subgngp  17983  ngptgp  17984  sranlm  18027  nlmvscnlem1  18029  nlmvscn  18030  nrginvrcn  18034  lssnlm  18043  nghmcn  18086  qtopbaslem  18099  reconn  18165  xmetdcn2  18174  metdscn  18192  metnrm  18198  elcncf1di  18231  cncffvrn  18234  mulc1cncf  18241  cncfco  18243  reparphti  18327  tchcph  18499  ipcnlem1  18504  ipcn  18505  iscfil3  18531  bcthlem5  18582  minveclem3  18625  minveclem7  18631  ovolicc2lem4  18711  dyadmbl  18787  volcn  18793  itg1addlem1  18879  itg1addlem2  18884  itg1addlem4  18886  mbfi1fseqlem1  18902  mbfi1fseqlem3  18904  mbfi1fseqlem4  18905  mbfi1fseqlem5  18906  dvmptfsum  19154  c1liplem1  19175  dvgt0lem2  19182  ftc1a  19216  evlseu  19232  ply1domn  19341  ply1divmo  19353  fta1b  19387  ig1peu  19389  coeeu  19439  plydivalg  19511  aaliou2b  19553  ulmss  19606  ulmcn  19608  efif1olem4  19739  logccv  19842  cvxcl  20111  basellem4  20153  fsumdvdscom  20257  musum  20263  dvdsmulf1o  20266  fsumdvdsmul  20267  dchrelbasd  20310  dchrmulcl  20320  dchrinv  20332  lgsqrlem2  20413  lgsdchr  20419  lgseisenlem2  20421  lgsquadlem1  20425  lgsquadlem2  20426  dchrisumlema  20469  dchrisumlem2  20471  chpdifbndlem2  20535  pntpbnd  20569  pntibndlem3  20573  isgrp2d  20732  grpoinvf  20737  subgoablo  20808  ghgrplem2  20864  ghablo  20866  nvmf  21034  vacn  21097  nmcvcn  21098  smcnlem  21100  sspg  21134  ssps  21136  sspmlem  21138  0lno  21198  blocni  21213  sspph  21263  ipblnfi  21264  minvecolem7  21292  unopf1o  22326  cnvunop  22328  unoplin  22330  counop  22331  hmopadj2  22351  hmoplin  22352  bralnfn  22358  lnopeq0i  22417  hmops  22430  hmopm  22431  hmopco  22433  lnconi  22443  cnlnadjlem2  22478  adjmul  22502  adjadd  22503  cdjreui  22842  erdszelem4  22896  erdszelem9  22901  erdsze2lem2  22906  cnpcon  22932  pconcon  22933  txpcon  22934  ptpcon  22935  cvxpcon  22944  cvxscon  22945  iccllyscon  22952  cvmseu  22978  cvmliftmo  22986  cvmlift2lem5  23009  cvmlift2lem9  23013  brbtwn2  23707  axlowdimlem15  23758  axcontlem2  23767  axcontlem10  23775  segconeu  23808  onsuct0  24054  toplat  24456  trooo  24560  rltrooo  24581  muldisc  24647  trnij  24781  sigadd  24815  fnmulcv  24850  icccon2  24866  icccon3  24867  icccon4  24868  idmon  24983  prismorcsetlemb  25079  setiscat  25145  fnessref  25459  neibastop1  25474  filnetlem3  25495  r19.21aivvaOLD  25504  sdclem1  25619  isbnd3  25674  prdsbnd  25683  ismtycnv  25692  ismtyhmeolem  25694  ismtyres  25698  bfplem1  25712  bfplem2  25713  bfp  25714  rrnmet  25719  ismrer1  25728  iccbnd  25730  grpokerinj  25741  isdrngo2  25755  rngogrphom  25768  rngohomco  25771  rngoisocnv  25778  iscringd  25790  erprt  25907  nacsfix  25953  rmxypairf1o  26162  wepwsolem  26304  dnnumch3  26310  fnwe2  26316  dsmmlss  26376  uvcf1  26407  frlmlbs  26415  lindff1  26456  lindfrn  26457  f1lindf  26458  mpaaeu  26521  issubmd  26549  mamucl  26622  mamudiagcl  26623  mamulid  26624  mamurid  26625  mamuass  26626  mamudi  26627  mamudir  26628  mamuvs1  26629  mamuvs2  26630  idomsubgmo  26680  mon1psubm  26691  deg1mhm  26692  lfl0f  27948  lkrlss  27974  lshpsmreu  27988  linepsubN  28630  pmapsub  28646  lautcnv  28968  lautco  28975  idltrn  29028  cdleme50f1  29421  cdleme50laut  29425  istendod  29640  dihf11  30146  dih1dimatlem  30208  lcfl7N  30380  lcfrlem9  30429  mapd1o  30527  hdmapf1oN  30747  hgmapf1oN  30785
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 2513
  Copyright terms: Public domain W3C validator