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

Theorem ralrimivva 2904
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 434 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ps ) )
32ralrimivv 2903 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1758   A.wral 2795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-ral 2800
This theorem is referenced by:  disjxiun  4387  swopo  4749  issod  4769  fcof1  6090  fliftfund  6105  soisores  6117  soisoi  6118  isocnv  6120  f1oiso  6141  caovclg  6355  caovcomg  6358  off  6434  caofrss  6453  caonncan  6458  dmmpt2g  6746  fnmpt2ovd  6751  fmpt2co  6756  poxp  6784  fvmpt2curryd  6890  smo11  6925  smoiso2  6930  omsmo  7193  qsdisj2  7278  eroprf  7298  dom2lem  7449  omxpenlem  7512  xpf1o  7573  unxpdomlem3  7620  fofinf1o  7693  dffi3  7782  supmo  7803  inf3lem6  7940  cantnf  8002  cantnfOLD  8024  rankxplim  8187  fseqenlem1  8295  fodomacn  8327  iunfictbso  8385  cofsmo  8539  infpssrlem5  8577  enfin2i  8591  fin23lem23  8596  fin23lem27  8598  fin23lem28  8610  compssiso  8644  ltordlem  9966  cju  10419  axdc4uzlem  11905  seqcaopr2  11943  seqhomo  11954  wrd2ind  12474  climcn2  13172  addcn2  13173  mulcn2  13175  o1of2  13192  isercolllem1  13244  fsum2dlem  13339  fsumcom2  13343  isprm6  13897  crt  13955  eulerthlem2  13959  vdwlem12  14155  cshwsdisj  14227  imasaddfnlem  14568  imasvscafn  14577  mreexexd  14688  iscatd  14713  proplem  14730  oppccomfpropd  14768  sectmon  14818  ssctr  14840  ssceq  14841  issubc3  14861  fullsubc  14862  fullresc  14863  isfuncd  14877  idfucl  14893  cofucl  14900  funcres2b  14909  fulloppc  14934  fthoppc  14935  idffth  14945  cofull  14946  cofth  14947  ressffth  14950  setcmon  15057  setcepi  15058  resssetc  15062  resscatc  15075  catciso  15077  evlfcl  15134  uncfcurf  15151  hofcl  15171  yonedalem3  15192  yonedainv  15193  yonffthlem  15194  yoniso  15197  isdrs2  15211  isposd  15227  pospropd  15406  poslubmo  15418  posglbmo  15419  mndplusf  15533  mndfo  15547  mndpropd  15548  issubmnd  15551  mhmpropd  15572  mhmf1o  15575  issubmd  15579  0mhm  15588  resmhm  15589  resmhm2  15590  resmhm2b  15591  mhmco  15592  submacs  15595  prdspjmhm  15597  pwsdiagmhm  15599  pwsco1mhm  15600  pwsco2mhm  15601  gsumwspan  15626  frmdsssubm  15641  frmdup1  15644  grpsubf  15707  issubg4  15802  grpissubg  15803  isnsg3  15817  nsgacs  15819  0nsg  15828  nsgid  15829  isghmd  15858  ghmmhm  15859  idghm  15864  ghmnsgima  15872  ghmnsgpreima  15873  ghmf1  15877  ghmf1o  15878  gaid  15919  subgga  15920  gass  15921  gasubg  15922  cntzsubm  15955  cntrsubgnsg  15960  lactghmga  16011  odf1  16167  sylow1lem2  16202  sylow2blem2  16224  sylow3lem1  16230  lsmssv  16246  lsmidm  16265  pj1eu  16297  efglem  16317  efgtf  16323  efgred  16349  efgredeu  16353  frgpmhm  16366  frgpuptf  16371  frgpuplem  16373  mulgmhm  16419  invghm  16422  ablnsg  16433  gsum2d2lem  16570  gsum2d2  16571  gsumcom2  16572  dprd2d2  16648  ablfaclem2  16692  srglmhm  16739  srgrmhm  16740  isrhm2d  16924  kerf1hrm  16937  issubrg2  16991  subrgint  16993  islmodd  17060  lmodscaf  17076  lmodprop2d  17113  islssd  17123  islss4  17149  lssacs  17154  lsspropd  17204  islmhmd  17226  lmhmima  17234  lmhmpreima  17235  reslmhm  17239  lspextmo  17243  lsmcl  17270  pj1lmhm  17287  islbs2  17341  issubrngd2  17376  opprdomn  17479  abvn0b  17480  issubassa2  17521  mvrf1  17605  mplsubglem  17617  mplsubglemOLD  17619  mplsubrg  17626  mplcoe5lem  17654  mplcoe2  17656  mplind  17691  evlslem2  17704  evlseu  17709  ply1sclf1  17850  expmhm  17989  nn0srg  17990  prmirredlem  18026  prmirredlemOLD  18029  expghm  18032  expghmOLD  18033  mulgghm2  18034  mulgghm2OLD  18037  domnchr  18072  znf1o  18093  zntoslem  18098  znfld  18102  cygznlem3  18111  phlipf  18190  dsmmlss  18278  uvcf1  18326  frlmlbs  18334  lindff1  18358  lindfrn  18359  f1lindf  18360  mamucl  18410  mamudiagcl  18411  mamulid  18413  mamurid  18414  mamuass  18415  mamudi  18416  mamudir  18417  mamuvs1  18418  mamuvs2  18419  matbas2d  18433  mavmul0g  18475  mdet1  18523  mdetunilem9  18542  mdetuni0  18543  mdetmul  18545  madutpos  18564  smadiadetlem4  18591  tgclb  18691  mretopd  18812  toponmre  18813  iscldtop  18815  ordtbaslem  18908  ordtbas2  18911  cnt0  19066  haust1  19072  cnhaus  19074  isreg2  19097  dishaus  19102  ordthaus  19104  dfcon2  19139  iuncon  19148  clscon  19150  2ndcomap  19178  dis2ndc  19180  llynlly  19197  restnlly  19202  restlly  19203  islly2  19204  llyidm  19208  nllyidm  19209  hausllycmp  19214  kgentopon  19227  txbas  19256  ptbasin2  19267  ptbasfi  19270  txcnp  19309  txcnmpt  19313  pthaus  19327  tx1stc  19339  xkococnlem  19348  xkococn  19349  cnmpt21  19360  qtoptop2  19388  qtopeu  19405  kqt0lem  19425  isr0  19426  regr1lem2  19429  kqreglem1  19430  kqreglem2  19431  kqnrmlem1  19432  kqnrmlem2  19433  nrmr0reg  19438  reghmph  19482  nrmhmph  19483  txswaphmeo  19494  qtophmeo  19506  fbun  19529  trfbas2  19532  isfil2  19545  infil  19552  trfil2  19576  filssufilg  19600  hausflim  19670  fclsnei  19708  fclsfnflim  19716  flimfnfcls  19717  ptcmplem1  19740  clssubg  19795  tgpconcomp  19799  divstgplem  19807  tsmsfbas  19814  utoptop  19925  iducn  19974  cstucnd  19975  isxmetd  20017  isxmet2d  20018  xmettpos  20040  prdsdsf  20058  prdsmet  20061  ressprdsds  20062  imasdsf1olem  20064  imasf1oxmet  20066  imasf1omet  20067  blfvalps  20074  xmetresbl  20128  metss2  20203  comet  20204  stdbdmet  20207  stdbdmopn  20209  methaus  20211  met2ndci  20213  metustfbasOLD  20256  metustfbas  20257  nrmmetd  20283  subgngp  20337  ngptgp  20338  sranlm  20381  nlmvscnlem1  20383  nlmvscn  20384  nrginvrcn  20388  lssnlm  20397  nghmcn  20440  qtopbaslem  20453  reconn  20521  xmetdcn2  20530  metdscn  20548  metnrm  20554  elcncf1di  20587  cncffvrn  20590  mulc1cncf  20597  cncfco  20599  reparphti  20685  tchcph  20868  ipcnlem1  20873  ipcn  20874  iscfil3  20900  bcthlem5  20955  rrxmet  21023  minveclem3  21032  minveclem7  21038  ovolicc2lem4  21119  dyadmbl  21196  volcn  21202  itg1addlem1  21286  itg1addlem2  21291  itg1addlem4  21293  mbfi1fseqlem1  21309  mbfi1fseqlem3  21311  mbfi1fseqlem4  21312  mbfi1fseqlem5  21313  dvmptfsum  21563  c1liplem1  21584  dvgt0lem2  21591  ftc1a  21625  ply1domn  21711  ply1divmo  21723  fta1b  21757  ig1peu  21759  coeeu  21809  plydivalg  21881  aaliou2b  21923  ulmss  21978  ulmcn  21980  efif1olem4  22117  logccv  22224  cvxcl  22494  basellem4  22537  fsumdvdscom  22641  musum  22647  dvdsmulf1o  22650  fsumdvdsmul  22651  dchrelbasd  22694  dchrmulcl  22704  dchrinv  22716  lgsqrlem2  22797  lgsdchr  22803  lgseisenlem2  22805  lgsquadlem1  22809  lgsquadlem2  22810  dchrisumlema  22853  dchrisumlem2  22855  chpdifbndlem2  22919  pntpbnd  22953  pntibndlem3  22957  axtgcont  23046  ercgrg  23088  tgisline  23155  tghilbert1_2  23166  mirreu3  23184  ragperp  23236  foot  23238  mideu  23245  f1otrgds  23250  f1otrg  23252  f1otrge  23253  xmstrkgc  23267  brbtwn2  23286  axlowdimlem15  23337  axcontlem2  23346  axcontlem10  23354  eengtrkg  23366  eengtrkge  23367  usgraedgreu  23441  usgraidx2v  23446  isgrp2d  23857  grpoinvf  23862  subgoablo  23933  ghgrplem2  23989  ghablo  23991  nvmf  24161  vacn  24224  nmcvcn  24225  smcnlem  24227  sspg  24261  ssps  24263  sspmlem  24265  0lno  24325  blocni  24340  sspph  24390  ipblnfi  24391  minvecolem7  24419  unopf1o  25455  cnvunop  25457  unoplin  25459  counop  25460  hmopadj2  25480  hmoplin  25481  bralnfn  25487  lnopeq0i  25546  hmops  25559  hmopm  25560  hmopco  25562  lnconi  25572  cnlnadjlem2  25607  adjmul  25631  adjadd  25632  cdjreui  25971  disjxpin  26064  off2  26093  f1od2  26158  xrofsup  26189  odutos  26258  abliso  26293  archiabllem1  26344  archiabllem2  26348  suborng  26417  xrge0slmod  26446  pstmxmet  26458  ofcf  26679  sibfof  26860  erdszelem4  27216  erdszelem9  27221  erdsze2lem2  27226  cnpcon  27253  pconcon  27254  txpcon  27255  ptpcon  27256  cvxpcon  27265  cvxscon  27266  iccllyscon  27273  cvmseu  27299  cvmliftmo  27307  cvmlift2lem5  27330  cvmlift2lem9  27334  fprodser  27596  fprod2dlem  27625  fprodcom2  27629  segconeu  28176  onsuct0  28421  fin2so  28554  heicant  28564  mblfinlem2  28567  ftc1anc  28613  fnessref  28703  neibastop1  28718  filnetlem3  28739  sdclem1  28777  isbnd3  28821  prdsbnd  28830  ismtycnv  28839  ismtyhmeolem  28841  ismtyres  28845  bfplem1  28859  bfplem2  28860  bfp  28861  rrnmet  28866  ismrer1  28875  iccbnd  28877  grpokerinj  28888  isdrngo2  28902  rngogrphom  28915  rngohomco  28918  rngoisocnv  28925  iscringd  28937  erprt  29156  nacsfix  29186  rmxypairf1o  29390  wepwsolem  29532  dnnumch3  29538  fnwe2  29544  mpaaeu  29645  idomsubgmo  29701  mon1psubm  29712  deg1mhm  29713  otsndisj  30269  otiunsndisj  30270  otiunsndisjX  30271  wlknwwlkninj  30481  wlkiswwlkinj  30488  wwlkextinj  30500  clwwlkf1  30596  2spotiundisj  30793  2spotmdisj  30799  numclwlk1lem2f1  30825  scmatscmidr  31012  dmatid  31028  dmatsubcl  31031  dmatsgrp  31032  dmatmulcl  31033  dmatsrng  31034  dmatcrng  31035  scmatsgrp  31039  scmatsrng  31041  scmatcrng  31042  scmatsgrp1  31043  scmatsrng1  31044  lindslinindsimp1  31098  lmod1  31141  1elcpmat  31178  cpmatacl  31179  cpmatmcl  31182  mat2pmatf1  31192  mat2pmatmul  31194  mat2pmat1  31195  mat2pmatlin  31198  m2cpm  31204  m2pminv  31211  m2pminv2  31213  pmatcollpw1dst  31228  pmatcollpw1  31232  monmatcollpw  31236  pmatcollpw3  31238  pmatcollpw4  31240  pmatcollpw4fi  31241  pmatcollpwscmatlem3  31247  mp2pm2mplem4  31264  pmattomply1f1  31267  pmattomply1mhmlem2  31274  cp0mat  31300  cpidmat  31301  lfl0f  33020  lkrlss  33046  lshpsmreu  33060  linepsubN  33702  pmapsub  33718  lautcnv  34040  lautco  34047  idltrn  34100  cdleme50f1  34493  cdleme50laut  34497  istendod  34712  dihf11  35218  dih1dimatlem  35280  lcfl7N  35452  lcfrlem9  35501  mapd1o  35599  hdmapf1oN  35819  hgmapf1oN  35857
  Copyright terms: Public domain W3C validator