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

Theorem ralrimivva 2781
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 435 . 2  |-  ( ph  ->  ( ( x  e.  A  /\  y  e.  B )  ->  ps ) )
32ralrimivv 2780 1  |-  ( ph  ->  A. x  e.  A  A. y  e.  B  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1872   A.wral 2709
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752
This theorem depends on definitions:  df-bi 188  df-an 372  df-ral 2714
This theorem is referenced by:  disjxiun  4358  otsndisj  4663  otiunsndisj  4664  swopo  4722  issod  4742  fcof1  6139  fliftfund  6160  soisores  6172  soisoi  6173  isocnv  6175  f1oiso  6196  oveqrspc2v  6267  caovclg  6414  caovcomg  6417  off  6499  caofrss  6517  caonncan  6522  dmmpt2g  6819  fnmpt2ovd  6824  fmpt2co  6829  poxp  6858  fvmpt2curryd  6968  smo11  7033  smoiso2  7038  omsmo  7305  qsdisj2  7391  eroprf  7411  dom2lem  7558  omxpenlem  7621  xpf1o  7682  unxpdomlem3  7726  fofinf1o  7800  dffi3  7893  supmo  7914  infmo  7959  inf3lem6  8086  cantnf  8145  rankxplim  8297  fseqenlem1  8401  fodomacn  8433  iunfictbso  8491  cofsmo  8645  infpssrlem5  8683  enfin2i  8697  fin23lem23  8702  fin23lem27  8704  fin23lem28  8716  compssiso  8750  ltordlem  10085  cju  10551  axdc4uzlem  12140  seqcaopr2  12194  seqhomo  12205  wrd2ind  12775  climcn2  13594  addcn2  13595  mulcn2  13597  o1of2  13614  isercolllem1  13666  fsum2dlem  13769  fsumcom2  13773  fprodser  13941  fprod2dlem  13972  fprodcom2  13976  isprm6  14604  crt  14664  eulerthlem2  14668  vdwlem12  14880  cshwsdisj  15007  imasaddfnlem  15372  imasvscafn  15381  mreexexd  15492  iscatd  15517  oppccomfpropd  15570  isofn  15618  sectmon  15625  ssctr  15668  ssceq  15669  catsubcat  15682  issubc3  15692  fullsubc  15693  fullresc  15694  isfuncd  15708  idfucl  15724  cofucl  15731  funcres2b  15740  fulloppc  15765  fthoppc  15766  idffth  15776  cofull  15777  cofth  15778  ressffth  15781  setcmon  15920  setcepi  15921  resssetc  15925  resscatc  15938  catciso  15940  fthestrcsetc  15973  fullestrcsetc  15974  embedsetcestrclem  15980  fthsetcestrc  15988  fullsetcestrc  15989  evlfcl  16045  uncfcurf  16062  hofcl  16082  yonedalem3  16103  yonedainv  16104  yonffthlem  16105  yoniso  16108  isdrs2  16122  isposd  16139  pospropd  16318  poslubmo  16330  posglbmo  16331  mgmplusf  16435  opifismgm  16439  ismndd  16497  mndpropd  16500  issubmnd  16502  mhmpropd  16526  idmhm  16529  mhmf1o  16530  issubmd  16534  0mhm  16543  resmhm  16544  resmhm2  16545  resmhm2b  16546  mhmco  16547  submacs  16550  prdspjmhm  16552  pwsdiagmhm  16554  pwsco1mhm  16555  pwsco2mhm  16556  gsumwspan  16568  frmdsssubm  16583  frmdup1  16586  grpsubf  16671  mhmmnd  16746  mhmfmhm  16747  issubg4  16774  grpissubg  16775  isnsg3  16789  nsgacs  16791  0nsg  16800  nsgid  16801  isghmd  16830  ghmmhm  16831  idghm  16836  ghmnsgima  16844  ghmnsgpreima  16845  ghmf1  16849  ghmf1o  16850  gaid  16891  subgga  16892  gass  16893  gasubg  16894  cntzsubm  16927  cntrsubgnsg  16932  lactghmga  16983  symgfixf1  17016  odf1  17151  sylow1lem2  17189  sylow2blem2  17211  sylow3lem1  17217  lsmssv  17233  lsmidm  17252  pj1eu  17284  efglem  17304  efgtf  17310  efgred  17336  efgredeu  17340  frgpmhm  17353  frgpuptf  17358  frgpuplem  17360  mulgmhm  17406  ghmcmn  17410  invghm  17412  ablnsg  17423  gsum2d2lem  17543  gsum2d2  17544  gsumcom2  17545  dprd2d2  17615  ablfaclem2  17657  srglmhm  17706  srgrmhm  17707  isrhm2d  17894  kerf1hrm  17909  issubrg2  17966  subrgint  17968  islmodd  18035  lmodscaf  18051  lmodprop2d  18088  islssd  18097  islss4  18123  lssacs  18128  lsspropd  18178  islmhmd  18200  lmhmima  18208  lmhmpreima  18209  reslmhm  18213  lspextmo  18217  lsmcl  18244  pj1lmhm  18261  islbs2  18315  issubrngd2  18350  opprdomn  18463  abvn0b  18464  issubassa2  18507  mvrf1  18587  mplsubglem  18596  mplsubrg  18602  mplcoe5lem  18629  mplcoe2  18631  mplind  18663  evlslem2  18673  evlseu  18677  ply1sclf1  18820  expmhm  18973  nn0srg  18974  prmirredlem  19001  expghm  19004  mulgghm2  19005  domnchr  19040  znf1o  19059  zntoslem  19064  znfld  19068  cygznlem3  19077  phlipf  19156  dsmmlss  19244  uvcf1  19287  frlmlbs  19292  lindff1  19315  lindfrn  19316  f1lindf  19317  mamucl  19363  mamuass  19364  mamudi  19365  mamudir  19366  mamuvs1  19367  mamuvs2  19368  matbas2d  19385  mamumat1cl  19401  mamulid  19403  mamurid  19404  mat1mhm  19446  dmatid  19457  dmatsubcl  19460  dmatsgrp  19461  dmatmulcl  19462  dmatsrng  19463  dmatcrng  19464  scmatscmiddistr  19470  scmatscm  19475  scmatsgrp  19481  scmatsrng  19482  scmatcrng  19483  scmatsgrp1  19484  scmatsrng1  19485  scmatf1  19493  scmatmhm  19496  mavmul0g  19515  mdet1  19563  mdetunilem9  19582  mdetuni0  19583  mdetmul  19585  madutpos  19604  smadiadetlem4  19631  1elcpmat  19676  cpmatacl  19677  cpmatmcl  19680  mat2pmatf1  19690  mat2pmatmul  19692  mat2pmat1  19693  mat2pmatlin  19696  m2cpm  19702  m2cpminvid  19714  m2cpminvid2  19716  decpmatmul  19733  pmatcollpw1  19737  monmatcollpw  19740  pmatcollpw  19742  pmatcollpw3lem  19744  pmatcollpwscmatlem2  19751  pm2mpf1  19760  mp2pm2mplem4  19770  pm2mpmhmlem2  19780  chp0mat  19807  chpidmat  19808  tgclb  19923  mretopd  20045  toponmre  20046  iscldtop  20048  ordtbaslem  20141  ordtbas2  20144  cnt0  20299  haust1  20305  cnhaus  20307  isreg2  20330  dishaus  20335  ordthaus  20337  dfcon2  20371  iuncon  20380  clscon  20382  2ndcomap  20410  dis2ndc  20412  llynlly  20429  restnlly  20434  restlly  20435  islly2  20436  llyidm  20440  nllyidm  20441  hausllycmp  20446  kgentopon  20490  txbas  20519  ptbasin2  20530  ptbasfi  20533  txcnp  20572  txcnmpt  20576  pthaus  20590  tx1stc  20602  xkococnlem  20611  xkococn  20612  cnmpt21  20623  qtoptop2  20651  qtopeu  20668  kqt0lem  20688  isr0  20689  regr1lem2  20692  kqreglem1  20693  kqreglem2  20694  kqnrmlem1  20695  kqnrmlem2  20696  nrmr0reg  20701  reghmph  20745  nrmhmph  20746  txswaphmeo  20757  qtophmeo  20769  fbun  20792  trfbas2  20795  isfil2  20808  infil  20815  trfil2  20839  filssufilg  20863  hausflim  20933  fclsnei  20971  fclsfnflim  20979  flimfnfcls  20980  ptcmplem1  21004  clssubg  21060  tgpconcomp  21064  qustgplem  21072  tsmsfbas  21079  utoptop  21186  iducn  21235  cstucnd  21236  isxmetd  21278  isxmet2d  21279  xmettpos  21301  prdsdsf  21319  prdsmet  21322  ressprdsds  21323  imasdsf1olem  21325  imasf1oxmet  21327  imasf1omet  21328  blfvalps  21335  xmetresbl  21389  metss2  21464  comet  21465  stdbdmet  21468  stdbdmopn  21470  methaus  21472  met2ndci  21474  metustfbas  21509  nrmmetd  21526  subgngp  21580  ngptgp  21581  sranlm  21624  nlmvscnlem1  21626  nlmvscn  21627  nrginvrcn  21631  lssnlm  21640  nghmcn  21703  qtopbaslem  21716  reconn  21783  xmetdcn2  21792  metdscn  21810  metdscnOLD  21825  metnrm  21831  elcncf1di  21864  cncffvrn  21867  mulc1cncf  21874  cncfco  21876  reparphti  21965  tchcph  22148  ipcnlem1  22153  ipcn  22154  iscfil3  22180  bcthlem5  22233  rrxmet  22299  minveclem3  22308  minveclem7  22314  minveclem3OLD  22320  minveclem7OLD  22326  ovolicc2lem4OLD  22410  ovolicc2lem4  22411  dyadmbl  22495  volcn  22501  itg1addlem1  22587  itg1addlem2  22592  itg1addlem4  22594  mbfi1fseqlem1  22610  mbfi1fseqlem3  22612  mbfi1fseqlem4  22613  mbfi1fseqlem5  22614  dvmptfsum  22864  c1liplem1  22885  dvgt0lem2  22892  ftc1a  22926  ply1domn  23009  ply1divmo  23023  fta1b  23057  ig1peu  23059  ig1peuOLD  23060  coeeu  23116  plydivalg  23189  aaliou2b  23234  ulmss  23289  ulmcn  23291  efif1olem4  23431  efsubm  23437  logccv  23545  logbmpt  23662  logbfval  23664  cvxcl  23847  basellem4  23947  fsumdvdscom  24051  musum  24057  dvdsmulf1o  24060  fsumdvdsmul  24061  dchrelbasd  24104  dchrmulcl  24114  dchrinv  24126  lgsqrlem2  24207  lgsdchr  24213  lgseisenlem2  24215  lgsquadlem1  24219  lgsquadlem2  24220  dchrisumlema  24263  dchrisumlem2  24265  chpdifbndlem2  24329  pntpbnd  24363  pntibndlem3  24367  axtgcont  24454  iscgrglt  24496  ercgrg  24499  idmot  24519  motco  24522  cnvmot  24523  motcgrg  24526  tgisline  24609  tghilberti2  24620  mirreu3  24636  mirmot  24657  ragperp  24699  foot  24701  mideu  24717  midf  24755  lmimot  24777  trgcopyeu  24785  f1otrgds  24836  f1otrg  24838  f1otrge  24839  xmstrkgc  24853  brbtwn2  24872  axlowdimlem15  24923  axcontlem2  24932  axcontlem10  24940  eengtrkg  24952  eengtrkge  24953  usgraedgreu  25052  usgraidx2v  25057  wlknwwlkninj  25376  wlkiswwlkinj  25383  wwlkextinj  25395  clwwlkf1  25461  clwlkf1clwwlk  25515  2spotiundisj  25727  2spotmdisj  25733  numclwlk1lem2f1  25759  isgrp2d  25900  grpoinvf  25905  subgoablo  25976  ghgrplem2OLD  26032  ghabloOLD  26034  nvmf  26204  vacn  26267  nmcvcn  26268  smcnlem  26270  sspg  26304  ssps  26306  sspmlem  26308  0lno  26368  blocni  26383  sspph  26433  ipblnfi  26434  minvecolem7  26462  minvecolem7OLD  26472  unopf1o  27506  cnvunop  27508  unoplin  27510  counop  27511  hmopadj2  27531  hmoplin  27532  bralnfn  27538  lnopeq0i  27597  hmops  27610  hmopm  27611  hmopco  27613  lnconi  27623  cnlnadjlem2  27658  adjmul  27682  adjadd  27683  cdjreui  28022  disjxpin  28139  off2  28183  f1od2  28254  xrofsup  28298  odutos  28370  abliso  28405  archiabllem1  28456  archiabllem2  28460  suborng  28525  xrge0slmod  28554  1smat1  28577  submateq  28582  madjusmdetlem3  28602  pstmxmet  28647  ofcf  28871  ldgenpisys  28935  rossros  28949  inelcarsg  29090  sibfof  29120  sitmf  29132  erdszelem4  29864  erdszelem9  29869  erdsze2lem2  29874  cnpcon  29900  pconcon  29901  txpcon  29902  ptpcon  29903  cvxpcon  29912  cvxscon  29913  iccllyscon  29920  cvmseu  29946  cvmliftmo  29954  cvmlift2lem5  29977  cvmlift2lem9  29981  mrsubff1  30099  elmrsubrn  30105  mrsubco  30106  msubff1  30141  mvhf1  30144  segconeu  30722  fnessref  30957  neibastop1  30959  filnetlem3  30980  onsuct0  31045  fin2so  31839  poimirlem4  31851  poimirlem13  31860  poimirlem14  31861  poimirlem26  31873  heicant  31882  mblfinlem2  31885  ftc1anc  31932  sdclem1  31979  isbnd3  32023  prdsbnd  32032  ismtycnv  32041  ismtyhmeolem  32043  ismtyres  32047  bfplem1  32061  bfplem2  32062  bfp  32063  rrnmet  32068  ismrer1  32077  iccbnd  32079  grpokerinj  32090  isdrngo2  32104  rngogrphom  32117  rngohomco  32120  rngoisocnv  32127  iscringd  32139  erprt  32356  lfl0f  32547  lkrlss  32573  lshpsmreu  32587  linepsubN  33229  pmapsub  33245  lautcnv  33567  lautco  33574  idltrn  33627  cdleme50f1  34022  cdleme50laut  34026  istendod  34241  dihf11  34747  dih1dimatlem  34809  lcfl7N  34981  lcfrlem9  35030  mapd1o  35128  hdmapf1oN  35348  hgmapf1oN  35386  nacsfix  35466  rmxypairf1o  35672  wepwsolem  35813  dnnumch3  35818  fnwe2  35824  mpaaeu  35929  idomsubgmo  35985  mon1psubm  35996  deg1mhm  35997  disjxp1  37327  disjf1  37361  wessf1ornlem  37363  projf1o  37378  sumnnodd  37593  lptioo2  37594  lptioo1  37595  cncfshift  37634  cncfperiod  37639  dvnprodlem1  37704  fourierdlem42  37895  fourierdlem42OLD  37896  nnfoctbdjlem  38144  isomennd  38203  iccpartgt  38554  icceuelpart  38563  otiunsndisjX  38814  usgredgreu  39045  usgredg2vtxeu  39047  usgridx2v  39051  usgvincvadeu  39308  usgvincvadeuALT  39311  usgedgvadf1  39318  usgedgvadf1ALT  39321  ismgmd  39367  mgmhmpropd  39376  mgmhmf1o  39378  idmgmhm  39379  issubmgm2  39381  rabsubmgmd  39382  resmgmhm  39389  resmgmhm2  39390  resmgmhm2b  39391  mgmhmco  39392  submgmacs  39395  opmpt2ismgm  39398  mgmplusgiopALT  39421  isrnghm2d  39492  c0mgm  39500  c0mhm  39501  lidlmmgm  39516  2zlidl  39525  rnghmsscmap2  39566  rnghmsscmap  39567  rnghmsubcsetclem2  39569  rhmsscmap2  39612  rhmsscmap  39613  rhmsubcsetclem2  39615  rhmsscrnghm  39619  rhmsubcrngclem2  39621  srhmsubc  39669  fldhmsubc  39677  rhmsubc  39683  srhmsubcALTV  39688  fldhmsubcALTV  39696  rhmsubcALTV  39702  lindslinindsimp1  39843
  Copyright terms: Public domain W3C validator