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

Theorem ralrimivva 2758
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 424 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ps ) )
32ralrimivv 2757 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721   A.wral 2666
This theorem is referenced by:  disjxiun  4169  swopo  4473  issod  4493  fcof1  5979  fliftfund  5994  soisores  6006  soisoi  6007  isocnv  6009  f1oiso  6030  caovclg  6198  caovcomg  6201  off  6279  caofrss  6296  caonncan  6301  fmpt2co  6389  poxp  6417  smo11  6585  smoiso2  6590  omsmo  6856  qsdisj2  6941  eroprf  6961  dom2lem  7106  omxpenlem  7168  xpf1o  7228  unxpdomlem3  7274  fofinf1o  7346  dffi3  7394  supmo  7413  inf3lem6  7544  cantnf  7605  rankxplim  7759  fseqenlem1  7861  fodomacn  7893  iunfictbso  7951  cofsmo  8105  infpssrlem5  8143  enfin2i  8157  fin23lem23  8162  fin23lem27  8164  fin23lem28  8176  compssiso  8210  ltordlem  9508  cju  9952  axdc4uzlem  11276  seqcaopr2  11314  seqhomo  11325  climcn2  12341  addcn2  12342  mulcn2  12344  o1of2  12361  isercolllem1  12413  fsum2dlem  12509  fsumcom2  12513  isprm6  13064  crt  13122  eulerthlem2  13126  vdwlem12  13315  imasaddfnlem  13708  imasvscafn  13717  mreexexd  13828  iscatd  13853  proplem  13870  oppccomfpropd  13908  sectmon  13958  ssctr  13980  ssceq  13981  issubc3  14001  fullsubc  14002  fullresc  14003  isfuncd  14017  idfucl  14033  cofucl  14040  funcres2b  14049  fulloppc  14074  fthoppc  14075  idffth  14085  cofull  14086  cofth  14087  ressffth  14090  setcmon  14197  setcepi  14198  resssetc  14202  resscatc  14215  catciso  14217  evlfcl  14274  uncfcurf  14291  hofcl  14311  yonedalem3  14332  yonedainv  14333  yonffthlem  14334  yoniso  14337  isdrs2  14351  isposd  14367  pospropd  14516  poslubmo  14528  mndplusf  14661  mndfo  14675  mndpropd  14676  issubmnd  14679  mhmpropd  14699  0mhm  14713  resmhm  14714  resmhm2  14715  resmhm2b  14716  mhmco  14717  submacs  14720  prdspjmhm  14721  pwsdiagmhm  14723  pwsco1mhm  14724  pwsco2mhm  14725  gsumwspan  14746  frmdsssubm  14761  frmdup1  14764  grpsubf  14823  issubg4  14916  isnsg3  14929  nsgacs  14931  0nsg  14940  nsgid  14941  isghmd  14970  ghmmhm  14971  idghm  14976  ghmnsgima  14984  ghmnsgpreima  14985  ghmf1  14989  ghmf1o  14990  gaid  15031  subgga  15032  gass  15033  gasubg  15034  lactghmga  15062  cntzsubm  15089  cntrsubgnsg  15094  odf1  15153  sylow1lem2  15188  sylow2blem2  15210  sylow3lem1  15216  lsmssv  15232  lsmidm  15251  pj1eu  15283  efglem  15303  efgtf  15309  efgred  15335  efgredeu  15339  frgpmhm  15352  frgpuptf  15357  frgpuplem  15359  mulgmhm  15405  invghm  15408  ablnsg  15417  gsum2d2lem  15502  gsum2d2  15503  gsumcom2  15504  dprd2d2  15557  ablfaclem2  15599  isrhm2d  15784  issubrg2  15843  subrgint  15845  islmodd  15911  lmodscaf  15927  lmodprop2d  15961  islssd  15967  islss4  15993  lssacs  15998  lsspropd  16048  islmhmd  16070  lmhmima  16078  lmhmpreima  16079  reslmhm  16083  lspextmo  16087  lsmcl  16110  pj1lmhm  16127  islbs2  16181  issubrngd2  16217  opprdomn  16316  abvn0b  16317  issubassa2  16358  mvrf1  16444  mplsubglem  16453  mplsubrg  16458  mplind  16517  evlslem2  16523  ply1sclf1  16635  prmirredlem  16728  expmhm  16731  expghm  16732  mulgghm2  16741  domnchr  16768  znf1o  16787  zntoslem  16792  znfld  16796  cygznlem3  16805  phlipf  16838  tgclb  16990  mretopd  17111  toponmre  17112  iscldtop  17114  ordtbaslem  17206  ordtbas2  17209  cnt0  17364  haust1  17370  cnhaus  17372  isreg2  17395  dishaus  17400  ordthaus  17402  dfcon2  17435  iuncon  17444  clscon  17446  2ndcomap  17474  dis2ndc  17476  llynlly  17493  restnlly  17498  restlly  17499  islly2  17500  llyidm  17504  nllyidm  17505  hausllycmp  17510  kgentopon  17523  txbas  17552  ptbasin2  17563  ptbasfi  17566  txcnp  17605  txcnmpt  17609  pthaus  17623  tx1stc  17635  xkococnlem  17644  xkococn  17645  cnmpt21  17656  qtoptop2  17684  qtopeu  17701  kqt0lem  17721  isr0  17722  regr1lem2  17725  kqreglem1  17726  kqreglem2  17727  kqnrmlem1  17728  kqnrmlem2  17729  nrmr0reg  17734  reghmph  17778  nrmhmph  17779  txswaphmeo  17790  qtophmeo  17802  fbun  17825  trfbas2  17828  isfil2  17841  infil  17848  trfil2  17872  filssufilg  17896  hausflim  17966  fclsnei  18004  fclsfnflim  18012  flimfnfcls  18013  ptcmplem1  18036  clssubg  18091  tgpconcomp  18095  divstgplem  18103  tsmsfbas  18110  utoptop  18217  iducn  18266  cstucnd  18267  isxmetd  18309  isxmet2d  18310  xmettpos  18332  prdsdsf  18350  prdsmet  18353  ressprdsds  18354  imasdsf1olem  18356  imasf1oxmet  18358  imasf1omet  18359  blfvalps  18366  xmetresbl  18420  metss2  18495  comet  18496  stdbdmet  18499  stdbdmopn  18501  methaus  18503  met2ndci  18505  metustfbasOLD  18548  metustfbas  18549  nrmmetd  18575  subgngp  18629  ngptgp  18630  sranlm  18673  nlmvscnlem1  18675  nlmvscn  18676  nrginvrcn  18680  lssnlm  18689  nghmcn  18732  qtopbaslem  18745  reconn  18812  xmetdcn2  18821  metdscn  18839  metnrm  18845  elcncf1di  18878  cncffvrn  18881  mulc1cncf  18888  cncfco  18890  reparphti  18975  tchcph  19147  ipcnlem1  19152  ipcn  19153  iscfil3  19179  bcthlem5  19234  minveclem3  19283  minveclem7  19289  ovolicc2lem4  19369  dyadmbl  19445  volcn  19451  itg1addlem1  19537  itg1addlem2  19542  itg1addlem4  19544  mbfi1fseqlem1  19560  mbfi1fseqlem3  19562  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  dvmptfsum  19812  c1liplem1  19833  dvgt0lem2  19840  ftc1a  19874  evlseu  19890  ply1domn  19999  ply1divmo  20011  fta1b  20045  ig1peu  20047  coeeu  20097  plydivalg  20169  aaliou2b  20211  ulmss  20266  ulmcn  20268  efif1olem4  20400  logccv  20507  cvxcl  20776  basellem4  20819  fsumdvdscom  20923  musum  20929  dvdsmulf1o  20932  fsumdvdsmul  20933  dchrelbasd  20976  dchrmulcl  20986  dchrinv  20998  lgsqrlem2  21079  lgsdchr  21085  lgseisenlem2  21087  lgsquadlem1  21091  lgsquadlem2  21092  dchrisumlema  21135  dchrisumlem2  21137  chpdifbndlem2  21201  pntpbnd  21235  pntibndlem3  21239  usgraedgreu  21360  usgraidx2v  21365  isgrp2d  21776  grpoinvf  21781  subgoablo  21852  ghgrplem2  21908  ghablo  21910  nvmf  22080  vacn  22143  nmcvcn  22144  smcnlem  22146  sspg  22180  ssps  22182  sspmlem  22184  0lno  22244  blocni  22259  sspph  22309  ipblnfi  22310  minvecolem7  22338  unopf1o  23372  cnvunop  23374  unoplin  23376  counop  23377  hmopadj2  23397  hmoplin  23398  bralnfn  23404  lnopeq0i  23463  hmops  23476  hmopm  23477  hmopco  23479  lnconi  23489  cnlnadjlem2  23524  adjmul  23548  adjadd  23549  cdjreui  23888  disjxpin  23981  off2  24007  xrofsup  24079  kerf1hrm  24215  pstmxmet  24245  ofcf  24439  sibfof  24607  erdszelem4  24833  erdszelem9  24838  erdsze2lem2  24843  cnpcon  24870  pconcon  24871  txpcon  24872  ptpcon  24873  cvxpcon  24882  cvxscon  24883  iccllyscon  24890  cvmseu  24916  cvmliftmo  24924  cvmlift2lem5  24947  cvmlift2lem9  24951  fprodser  25228  fprod2dlem  25257  fprodcom2  25261  brbtwn2  25748  axlowdimlem15  25799  axcontlem2  25808  axcontlem10  25816  segconeu  25849  onsuct0  26095  mblfinlem  26143  fnessref  26263  neibastop1  26278  filnetlem3  26299  sdclem1  26337  isbnd3  26383  prdsbnd  26392  ismtycnv  26401  ismtyhmeolem  26403  ismtyres  26407  bfplem1  26421  bfplem2  26422  bfp  26423  rrnmet  26428  ismrer1  26437  iccbnd  26439  grpokerinj  26450  isdrngo2  26464  rngogrphom  26477  rngohomco  26480  rngoisocnv  26487  iscringd  26499  erprt  26612  nacsfix  26656  rmxypairf1o  26864  wepwsolem  27006  dnnumch3  27012  fnwe2  27018  dsmmlss  27078  uvcf1  27109  frlmlbs  27117  lindff1  27158  lindfrn  27159  f1lindf  27160  mpaaeu  27223  issubmd  27251  mamucl  27324  mamudiagcl  27325  mamulid  27326  mamurid  27327  mamuass  27328  mamudi  27329  mamudir  27330  mamuvs1  27331  mamuvs2  27332  idomsubgmo  27382  mon1psubm  27393  deg1mhm  27394  dmmpt2g  27850  otsndisj  27953  otiunsndisj  27954  otiunsndisjX  27955  2spotiundisj  28165  2spotmdisj  28171  lfl0f  29552  lkrlss  29578  lshpsmreu  29592  linepsubN  30234  pmapsub  30250  lautcnv  30572  lautco  30579  idltrn  30632  cdleme50f1  31025  cdleme50laut  31029  istendod  31244  dihf11  31750  dih1dimatlem  31812  lcfl7N  31984  lcfrlem9  32033  mapd1o  32131  hdmapf1oN  32351  hgmapf1oN  32389
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2671
  Copyright terms: Public domain W3C validator