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

Theorem ralrimivva 2606
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 2605 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 2516
This theorem is referenced by:  disjxiun  3960  swopo  4261  issod  4281  fcof1  5696  fliftfund  5711  soisores  5723  soisoi  5724  isocnv  5726  f1oiso  5747  caovclg  5911  caovcomg  5914  off  5992  caofrss  6009  caonncan  6014  fmpt2co  6101  poxp  6126  smo11  6314  smoiso2  6319  omsmo  6585  qsdisj2  6670  eroprf  6689  dom2lem  6834  omxpenlem  6896  xpf1o  6956  unxpdomlem3  7002  fofinf1o  7070  dffi3  7117  inf3lem6  7267  cantnf  7328  rankxplim  7482  fseqenlem1  7584  fodomacn  7616  iunfictbso  7674  cofsmo  7828  infpssrlem5  7866  enfin2i  7880  fin23lem23  7885  fin23lem27  7887  fin23lem28  7899  compssiso  7933  ltordlem  9231  cju  9675  axdc4uzlem  10975  seqcaopr2  11013  seqhomo  11024  climcn2  11996  addcn2  11997  mulcn2  11999  o1of2  12016  isercolllem1  12068  fsum2dlem  12163  fsumcom2  12167  isprm6  12715  crt  12773  eulerthlem2  12777  vdwlem12  12966  imasaddfnlem  13357  imasvscafn  13366  mreexexd  13477  iscatd  13502  proplem  13519  oppccomfpropd  13557  sectmon  13607  ssctr  13629  ssceq  13630  issubc3  13650  fullsubc  13651  fullresc  13652  isfuncd  13666  idfucl  13682  cofucl  13689  funcres2b  13698  fulloppc  13723  fthoppc  13724  idffth  13734  cofull  13735  cofth  13736  ressffth  13739  setcmon  13846  setcepi  13847  resssetc  13851  resscatc  13864  catciso  13866  evlfcl  13923  uncfcurf  13940  hofcl  13960  yonedalem3  13981  yonedainv  13982  yonffthlem  13983  yoniso  13986  isdrs2  14000  isposd  14016  pospropd  14165  poslubmo  14177  mndplusf  14310  mndfo  14324  mndpropd  14325  issubmnd  14328  mhmpropd  14348  0mhm  14362  resmhm  14363  resmhm2  14364  resmhm2b  14365  mhmco  14366  submacs  14369  prdspjmhm  14370  pwsdiagmhm  14372  pwsco1mhm  14373  pwsco2mhm  14374  gsumwspan  14395  frmdsssubm  14410  frmdup1  14413  grpsubf  14472  issubg4  14565  isnsg3  14578  nsgacs  14580  0nsg  14589  nsgid  14590  isghmd  14619  ghmmhm  14620  idghm  14625  ghmnsgima  14633  ghmnsgpreima  14634  ghmf1  14638  ghmf1o  14639  gaid  14680  subgga  14681  gass  14682  gasubg  14683  lactghmga  14711  cntzsubm  14738  cntrsubgnsg  14743  odf1  14802  sylow1lem2  14837  sylow2blem2  14859  sylow3lem1  14865  lsmssv  14881  lsmidm  14900  pj1eu  14932  efglem  14952  efgtf  14958  efgred  14984  efgredeu  14988  frgpmhm  15001  frgpuptf  15006  frgpuplem  15008  mulgmhm  15054  invghm  15057  ablnsg  15066  gsum2d2lem  15151  gsum2d2  15152  gsumcom2  15153  dprd2d2  15206  ablfaclem2  15248  isrhm2d  15433  issubrg2  15492  subrgint  15494  islmodd  15560  lmodscaf  15576  lmodprop2d  15614  islssd  15620  islss4  15646  lssacs  15651  lsspropd  15701  islmhmd  15723  lmhmima  15731  lmhmpreima  15732  reslmhm  15736  lspextmo  15740  lsmcl  15763  pj1lmhm  15780  islbs2  15834  issubrngd2  15870  opprdomn  15969  abvn0b  15970  issubassa2  16011  mvrf1  16097  mplsubglem  16106  mplsubrg  16111  mplind  16170  evlslem2  16176  ply1sclf1  16291  prmirredlem  16373  expmhm  16376  expghm  16377  mulgghm2  16386  domnchr  16413  znf1o  16432  zntoslem  16437  znfld  16441  cygznlem3  16450  phlipf  16483  tgclb  16635  mretopd  16756  toponmre  16757  iscldtop  16759  ordtbaslem  16845  ordtbas2  16848  cnt0  17001  haust1  17007  cnhaus  17009  isreg2  17032  dishaus  17037  ordthaus  17039  dfcon2  17072  iuncon  17081  clscon  17083  2ndcomap  17111  dis2ndc  17113  llynlly  17130  restnlly  17135  restlly  17136  islly2  17137  llyidm  17141  nllyidm  17142  hausllycmp  17147  kgentopon  17160  txbas  17189  ptbasin2  17200  ptbasfi  17203  txcnp  17241  txcnmpt  17245  pthaus  17259  tx1stc  17271  xkococnlem  17280  xkococn  17281  cnmpt21  17292  qtoptop2  17317  qtopeu  17334  kqt0lem  17354  isr0  17355  regr1lem2  17358  kqreglem1  17359  kqreglem2  17360  kqnrmlem1  17361  kqnrmlem2  17362  nrmr0reg  17367  reghmph  17411  nrmhmph  17412  txswaphmeo  17423  qtophmeo  17435  fbun  17462  trfbas2  17465  isfil2  17478  infil  17485  trfil2  17509  filssufilg  17533  hausflim  17603  fclsnei  17641  fclsfnflim  17649  flimfnfcls  17650  ptcmplem1  17673  clssubg  17718  tgpconcomp  17722  divstgplem  17730  tsmsfbas  17737  isxmetd  17818  isxmet2d  17819  xmettpos  17840  prdsdsf  17858  prdsmet  17861  ressprdsds  17862  imasdsf1olem  17864  imasf1oxmet  17866  imasf1omet  17867  blfval  17874  xmetresbl  17910  metss2  17985  comet  17986  stdbdmet  17989  stdbdmopn  17991  methaus  17993  met2ndci  17995  nrmmetd  18024  subgngp  18078  ngptgp  18079  sranlm  18122  nlmvscnlem1  18124  nlmvscn  18125  nrginvrcn  18129  lssnlm  18138  nghmcn  18181  qtopbaslem  18194  reconn  18260  xmetdcn2  18269  metdscn  18287  metnrm  18293  elcncf1di  18326  cncffvrn  18329  mulc1cncf  18336  cncfco  18338  reparphti  18422  tchcph  18594  ipcnlem1  18599  ipcn  18600  iscfil3  18626  bcthlem5  18677  minveclem3  18720  minveclem7  18726  ovolicc2lem4  18806  dyadmbl  18882  volcn  18888  itg1addlem1  18974  itg1addlem2  18979  itg1addlem4  18981  mbfi1fseqlem1  18997  mbfi1fseqlem3  18999  mbfi1fseqlem4  19000  mbfi1fseqlem5  19001  dvmptfsum  19249  c1liplem1  19270  dvgt0lem2  19277  ftc1a  19311  evlseu  19327  ply1domn  19436  ply1divmo  19448  fta1b  19482  ig1peu  19484  coeeu  19534  plydivalg  19606  aaliou2b  19648  ulmss  19701  ulmcn  19703  efif1olem4  19834  logccv  19937  cvxcl  20206  basellem4  20248  fsumdvdscom  20352  musum  20358  dvdsmulf1o  20361  fsumdvdsmul  20362  dchrelbasd  20405  dchrmulcl  20415  dchrinv  20427  lgsqrlem2  20508  lgsdchr  20514  lgseisenlem2  20516  lgsquadlem1  20520  lgsquadlem2  20521  dchrisumlema  20564  dchrisumlem2  20566  chpdifbndlem2  20630  pntpbnd  20664  pntibndlem3  20668  isgrp2d  20827  grpoinvf  20832  subgoablo  20903  ghgrplem2  20959  ghablo  20961  nvmf  21129  vacn  21192  nmcvcn  21193  smcnlem  21195  sspg  21229  ssps  21231  sspmlem  21233  0lno  21293  blocni  21308  sspph  21358  ipblnfi  21359  minvecolem7  21387  unopf1o  22421  cnvunop  22423  unoplin  22425  counop  22426  hmopadj2  22446  hmoplin  22447  bralnfn  22453  lnopeq0i  22512  hmops  22525  hmopm  22526  hmopco  22528  lnconi  22538  cnlnadjlem2  22573  adjmul  22597  adjadd  22598  cdjreui  22937  erdszelem4  23062  erdszelem9  23067  erdsze2lem2  23072  cnpcon  23098  pconcon  23099  txpcon  23100  ptpcon  23101  cvxpcon  23110  cvxscon  23111  iccllyscon  23118  cvmseu  23144  cvmliftmo  23152  cvmlift2lem5  23175  cvmlift2lem9  23179  brbtwn2  23873  axlowdimlem15  23924  axcontlem2  23933  axcontlem10  23941  segconeu  23974  onsuct0  24220  toplat  24622  trooo  24726  rltrooo  24747  muldisc  24813  trnij  24947  sigadd  24981  fnmulcv  25016  icccon2  25032  icccon3  25033  icccon4  25034  idmon  25149  prismorcsetlemb  25245  setiscat  25311  fnessref  25625  neibastop1  25640  filnetlem3  25661  r19.21aivvaOLD  25670  sdclem1  25785  isbnd3  25840  prdsbnd  25849  ismtycnv  25858  ismtyhmeolem  25860  ismtyres  25864  bfplem1  25878  bfplem2  25879  bfp  25880  rrnmet  25885  ismrer1  25894  iccbnd  25896  grpokerinj  25907  isdrngo2  25921  rngogrphom  25934  rngohomco  25937  rngoisocnv  25944  iscringd  25956  erprt  26073  nacsfix  26119  rmxypairf1o  26328  wepwsolem  26470  dnnumch3  26476  fnwe2  26482  dsmmlss  26542  uvcf1  26573  frlmlbs  26581  lindff1  26622  lindfrn  26623  f1lindf  26624  mpaaeu  26687  issubmd  26715  mamucl  26788  mamudiagcl  26789  mamulid  26790  mamurid  26791  mamuass  26792  mamudi  26793  mamudir  26794  mamuvs1  26795  mamuvs2  26796  idomsubgmo  26846  mon1psubm  26857  deg1mhm  26858  lfl0f  28389  lkrlss  28415  lshpsmreu  28429  linepsubN  29071  pmapsub  29087  lautcnv  29409  lautco  29416  idltrn  29469  cdleme50f1  29862  cdleme50laut  29866  istendod  30081  dihf11  30587  dih1dimatlem  30649  lcfl7N  30821  lcfrlem9  30870  mapd1o  30968  hdmapf1oN  31188  hgmapf1oN  31226
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 2520
  Copyright terms: Public domain W3C validator