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

Theorem ralrimivva 3188
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 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝜓)
Assertion
Ref Expression
ralrimivva (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Distinct variable groups:   𝜑,𝑥,𝑦   𝑦,𝐴
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem ralrimivva
StepHypRef Expression
1 ralrimivva.1 . . 3 ((𝜑 ∧ (𝑥𝐴𝑦𝐵)) → 𝜓)
21ex 413 . 2 (𝜑 → ((𝑥𝐴𝑦𝐵) → 𝜓))
32ralrimivv 3187 1 (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105  wral 3135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem depends on definitions:  df-bi 208  df-an 397  df-ral 3140
This theorem is referenced by:  disjord  5045  disjxiun  5054  otsndisj  5400  otiunsndisj  5401  swopo  5477  issod  5499  reuop  6137  fcof1  7034  fliftfund  7055  isof1oidb  7066  isof1oopb  7067  soisores  7069  soisoi  7070  isocnv  7072  f1oiso  7093  oveqrspc2v  7172  oprres  7305  caovclg  7329  caovcomg  7332  off  7413  caofrss  7431  caonncan  7436  dmmpog  7761  fnmpoovd  7771  fmpoco  7779  fsplitfpar  7803  poxp  7811  fvmpocurryd  7926  smo11  7990  smoiso2  7995  omsmo  8270  qsdisj2  8364  eroprf  8384  dom2lem  8537  omxpenlem  8606  xpf1o  8667  unxpdomlem3  8712  fofinf1o  8787  dffi3  8883  supmo  8904  infmo  8947  inf3lem6  9084  cantnf  9144  rankxplim  9296  fseqenlem1  9438  fodomacn  9470  iunfictbso  9528  cofsmo  9679  infpssrlem5  9717  enfin2i  9731  fin23lem23  9736  fin23lem27  9738  fin23lem28  9750  compssiso  9784  ltordlem  11153  cju  11622  axdc4uzlem  13339  seqcaopr2  13394  seqhomo  13405  wrd2ind  14073  cshf1  14160  s3sndisj  14315  s3iunsndisj  14316  climcn2  14937  addcn2  14938  mulcn2  14940  o1of2  14957  isercolllem1  15009  fsum2dlem  15113  fsumcom2  15117  fprodser  15291  fprod2dlem  15322  fprodcom2  15326  isprm6  16046  crth  16103  eulerthlem2  16107  vdwlem12  16316  cshwsdisj  16420  imasaddfnlem  16789  imasvscafn  16798  mreexexd  16907  iscatd  16932  oppccomfpropd  16985  isofn  17033  sectmon  17040  ssctr  17083  ssceq  17084  catsubcat  17097  issubc3  17107  fullsubc  17108  fullresc  17109  isfuncd  17123  idfucl  17139  cofucl  17146  funcres2b  17155  fulloppc  17180  fthoppc  17181  idffth  17191  cofull  17192  cofth  17193  ressffth  17196  setcmon  17335  setcepi  17336  resssetc  17340  resscatc  17353  catciso  17355  fthestrcsetc  17388  fullestrcsetc  17389  embedsetcestrclem  17395  fthsetcestrc  17403  fullsetcestrc  17404  evlfcl  17460  uncfcurf  17477  hofcl  17497  yonedalem3  17518  yonedainv  17519  yonffthlem  17520  yoniso  17523  isdrs2  17537  isposd  17553  pospropd  17732  poslubmo  17744  posglbmo  17745  mgmplusf  17850  issstrmgm  17851  opifismgm  17857  ismndd  17921  mndpropd  17924  issubmnd  17926  mndinvmod  17929  mhmpropd  17950  idmhm  17953  mhmf1o  17954  issubmd  17959  mndissubm  17960  0mhm  17972  resmhm  17973  resmhm2  17974  resmhm2b  17975  mhmco  17976  submacs  17979  prdspjmhm  17981  pwsdiagmhm  17983  pwsco1mhm  17984  pwsco2mhm  17985  gsumwspan  17999  frmdsssubm  18014  frmdup1  18017  grpsubf  18116  dfgrp3  18136  mhmmnd  18159  mhmfmhm  18160  issubg4  18236  grpissubg  18237  isnsg3  18250  nsgacs  18252  0nsg  18259  nsgid  18260  cycsubmcom  18285  isghmd  18305  ghmmhm  18306  idghm  18311  ghmnsgima  18320  ghmnsgpreima  18321  ghmf1  18325  ghmf1o  18326  gaid  18367  subgga  18368  gass  18369  gasubg  18370  cntzsubm  18404  cntrsubgnsg  18409  lactghmga  18462  symgfixf1  18494  odf1  18618  sylow1lem2  18653  sylow2blem2  18675  sylow3lem1  18681  lsmssv  18697  smndlsmidm  18710  lsmidmOLD  18718  pj1eu  18751  efglem  18771  efgtf  18777  efgred  18803  efgredeu  18807  frgpmhm  18820  frgpuptf  18825  frgpuplem  18827  mulgmhm  18877  ghmcmn  18881  invghm  18883  ablnsg  18896  cygabl  18939  gsum2d2lem  19022  gsum2d2  19023  gsumcom2  19024  dprd2d2  19095  ablfaclem2  19137  srgfcl  19194  srglmhm  19214  srgrmhm  19215  isrhm2d  19409  kerf1ghm  19426  kerf1hrmOLD  19427  issubrg2  19484  subrgint  19486  primefld  19513  islmodd  19569  lmodscaf  19585  lmodprop2d  19625  islssd  19636  islss4  19663  lssacs  19668  lsspropd  19718  islmhmd  19740  lmhmima  19748  lmhmpreima  19749  reslmhm  19753  lspextmo  19757  lsmcl  19784  pj1lmhm  19801  islbs2  19855  issubrngd2  19890  opprdomn  20002  abvn0b  20003  issubassa2  20049  mvrf1  20133  mplsubglem  20142  mplsubrg  20148  mplcoe5lem  20176  mplcoe2  20178  mplind  20210  evlslem2  20220  evlseu  20224  mhplss  20270  ply1sclf1  20385  expmhm  20542  nn0srg  20543  prmirredlem  20568  expghm  20571  mulgghm2  20572  domnchr  20607  znf1o  20626  zntoslem  20631  znfld  20635  cygznlem3  20644  phlipf  20724  dsmmlss  20816  uvcf1  20864  frlmlbs  20869  lindff1  20892  lindfrn  20893  f1lindf  20894  mamucl  20938  mamuass  20939  mamudi  20940  mamudir  20941  mamuvs1  20942  mamuvs2  20943  matbas2d  20960  mamumat1cl  20976  mamulid  20978  mamurid  20979  mat1mhm  21021  dmatid  21032  dmatsubcl  21035  dmatsgrp  21036  dmatmulcl  21037  dmatsrng  21038  dmatcrng  21039  scmatscmiddistr  21045  scmatscm  21050  scmatsgrp  21056  scmatsrng  21057  scmatcrng  21058  scmatsgrp1  21059  scmatsrng1  21060  scmatf1  21068  scmatmhm  21071  mavmul0g  21090  mdet1  21138  mdetunilem9  21157  mdetuni0  21158  mdetmul  21160  madutpos  21179  smadiadetlem4  21206  1elcpmat  21251  cpmatacl  21252  cpmatmcl  21255  mat2pmatf1  21265  mat2pmatmul  21267  mat2pmat1  21268  mat2pmatlin  21271  m2cpm  21277  m2cpminvid  21289  m2cpminvid2  21291  decpmatmul  21308  pmatcollpw1  21312  monmatcollpw  21315  pmatcollpw  21317  pmatcollpw3lem  21319  pmatcollpwscmatlem2  21326  pm2mpf1  21335  mp2pm2mplem4  21345  pm2mpmhmlem2  21355  chp0mat  21382  chpidmat  21383  tgclb  21506  mretopd  21628  toponmre  21629  iscldtop  21631  ordtbaslem  21724  ordtbas2  21727  cnt0  21882  haust1  21888  cnhaus  21890  isreg2  21913  dishaus  21918  ordthaus  21920  dfconn2  21955  iunconn  21964  clsconn  21966  2ndcomap  21994  dis2ndc  21996  llynlly  22013  restnlly  22018  restlly  22019  islly2  22020  llyidm  22024  nllyidm  22025  hausllycmp  22030  kgentopon  22074  txbas  22103  ptbasin2  22114  ptbasfi  22117  txcnp  22156  txcnmpt  22160  pthaus  22174  tx1stc  22186  xkococnlem  22195  xkococn  22196  cnmpt21  22207  qtoptop2  22235  qtopeu  22252  kqt0lem  22272  isr0  22273  regr1lem2  22276  kqreglem1  22277  kqreglem2  22278  kqnrmlem1  22279  kqnrmlem2  22280  nrmr0reg  22285  reghmph  22329  nrmhmph  22330  txswaphmeo  22341  qtophmeo  22353  fbun  22376  trfbas2  22379  isfil2  22392  infil  22399  trfil2  22423  filssufilg  22447  hausflim  22517  fclsnei  22555  fclsfnflim  22563  flimfnfcls  22564  ptcmplem1  22588  clssubg  22644  tgpconncomp  22648  qustgplem  22656  tsmsfbas  22663  utoptop  22770  iducn  22819  cstucnd  22820  isxmetd  22863  isxmet2d  22864  xmettpos  22886  prdsdsf  22904  prdsmet  22907  ressprdsds  22908  imasdsf1olem  22910  imasf1oxmet  22912  imasf1omet  22913  blfvalps  22920  xmetresbl  22974  metss2  23049  comet  23050  stdbdmet  23053  stdbdmopn  23055  methaus  23057  met2ndci  23059  metustfbas  23094  nrmmetd  23111  subgngp  23171  ngptgp  23172  sranlm  23220  nlmvscnlem1  23222  nlmvscn  23223  nrginvrcn  23228  lssnlm  23237  nghmcn  23281  qtopbaslem  23294  reconn  23363  xmetdcn2  23372  metdscn  23391  metnrm  23397  elcncf1di  23430  cncffvrn  23433  mulc1cncf  23440  cncfco  23442  reparphti  23528  isncvsngpd  23681  tcphcph  23767  ipcnlem1  23775  ipcn  23776  iscfil3  23803  bcthlem5  23858  rrxmet  23938  minveclem3  23959  minveclem7  23965  ovolicc2lem4  24048  dyadmbl  24128  volcn  24134  itg1addlem1  24220  itg1addlem2  24225  itg1addlem4  24227  mbfi1fseqlem1  24243  mbfi1fseqlem3  24245  mbfi1fseqlem4  24246  mbfi1fseqlem5  24247  dvmptfsum  24499  c1liplem1  24520  dvgt0lem2  24527  ftc1a  24561  ply1domn  24644  ply1divmo  24656  fta1b  24690  ig1peu  24692  coeeu  24742  plydivalg  24815  aaliou2b  24857  ulmss  24912  ulmcn  24914  efif1olem4  25056  efsubm  25062  logccv  25173  logbmpt  25293  logbfval  25295  cvxcl  25489  basellem4  25588  fsumdvdscom  25689  musum  25695  dvdsmulf1o  25698  fsumdvdsmul  25699  dchrelbasd  25742  dchrmulcl  25752  dchrinv  25764  lgsqrlem2  25850  lgsdchr  25858  lgseisenlem2  25879  lgsquadlem1  25883  lgsquadlem2  25884  2sqreulem4  25957  dchrisumlema  25991  dchrisumlem2  25993  chpdifbndlem2  26057  pntpbnd  26091  pntibndlem3  26095  axtgcont  26182  tgjustc1  26188  tgjustc2  26189  iscgrglt  26227  ercgrg  26230  idmot  26250  motco  26253  cnvmot  26254  motcgrg  26257  tgisline  26340  tghilberti2  26351  mirreu3  26367  mirmot  26388  ragperp  26430  foot  26435  mideu  26451  midf  26489  lmimot  26511  trgcopyeu  26519  f1otrgds  26582  f1otrg  26584  f1otrge  26585  xmstrkgc  26599  brbtwn2  26618  axlowdimlem15  26669  axcontlem2  26678  axcontlem10  26686  eengtrkg  26699  eengtrkge  26700  numedglnl  26856  usgredgreu  26927  uspgredg2vtxeu  26929  uspgredg2v  26933  usgredg2v  26936  wlkswwlksf1o  27584  wwlksnextinj  27604  clwlkclwwlkf1  27715  clwwlkf1  27755  frcond4  27976  frgrncvvdeqlem8  28012  frgrncvvdeq  28015  frgrwopreglem4  28021  numclwwlk1lem2f1  28063  grpoinvf  28236  nvmf  28349  vacn  28398  nmcvcn  28399  smcnlem  28401  sspg  28432  ssps  28434  sspmlem  28436  0lno  28494  blocni  28509  ipblnfi  28559  minvecolem7  28587  unopf1o  29620  cnvunop  29622  unoplin  29624  counop  29625  hmopadj2  29645  hmoplin  29646  bralnfn  29652  lnopeq0i  29711  hmops  29724  hmopm  29725  hmopco  29727  lnconi  29737  cnlnadjlem2  29772  adjmul  29796  adjadd  29797  cdjreui  30136  disjxpin  30266  off2  30316  fnpreimac  30344  suppovss  30354  f1od2  30383  xrofsup  30418  s3f1  30550  ccatf1  30552  swrdf1  30557  odutos  30577  abliso  30610  symgcntz  30656  tocyccntz  30713  archiabllem1  30749  archiabllem2  30753  suborng  30815  xrge0slmod  30844  prmidl2  30877  isprmidlc  30881  qsidomlem1  30882  qsidomlem2  30883  lindsun  30920  fedgmullem1  30924  fedgmullem2  30925  fedgmul  30926  1smat1  30968  submateq  30973  madjusmdetlem3  30993  pstmxmet  31036  ofcf  31261  ldgenpisys  31324  rossros  31338  inelcarsg  31468  sibfof  31497  sitmf  31509  hgt750lemb  31826  erdszelem4  32338  erdszelem9  32343  erdsze2lem2  32348  cnpconn  32374  pconnconn  32375  txpconn  32376  ptpconn  32377  cvxpconn  32386  cvxsconn  32387  iccllysconn  32394  cvmseu  32420  cvmliftmo  32428  cvmlift2lem5  32451  cvmlift2lem9  32455  mrsubff1  32658  elmrsubrn  32664  mrsubco  32665  msubff1  32700  mvhf1  32703  sslttr  33165  segconeu  33369  fnessref  33602  neibastop1  33604  filnetlem3  33625  onsuct0  33686  unblimceq0lem  33742  unbdqndv2  33747  knoppndv  33770  uncf  34752  fin2so  34760  lindsadd  34766  poimirlem4  34777  poimirlem13  34786  poimirlem14  34787  poimirlem26  34799  heicant  34808  mblfinlem2  34811  ftc1anc  34856  sdclem1  34899  isbnd3  34943  prdsbnd  34952  ismtycnv  34961  ismtyhmeolem  34963  ismtyres  34967  bfplem1  34981  bfplem2  34982  bfp  34983  rrnmet  34988  ismrer1  34997  iccbnd  34999  grpokerinj  35052  isdrngo2  35117  rngogrphom  35130  rngohomco  35133  rngoisocnv  35140  iscringd  35157  erprt  35889  lfl0f  36085  lkrlss  36111  lshpsmreu  36125  linepsubN  36768  pmapsub  36784  lautcnv  37106  lautco  37113  idltrn  37166  cdleme50f1  37559  cdleme50laut  37563  istendod  37778  dihf11  38283  dih1dimatlem  38345  lcfl7N  38517  lcfrlem9  38566  mapd1o  38664  hdmapf1oN  38881  hgmapf1oN  38919  qsalrel  39003  nacsfix  39187  rmxypairf1o  39386  wepwsolem  39520  dnnumch3  39525  fnwe2  39531  mpaaeu  39628  idomsubgmo  39676  mon1psubm  39684  deg1mhm  39685  isotone1  40276  isotone2  40277  disjxp1  41208  disjf1  41319  wessf1ornlem  41321  projf1o  41335  sumnnodd  41787  lptioo2  41788  lptioo1  41789  cncfshift  42033  cncfperiod  42038  dvnprodlem1  42107  fourierdlem42  42311  nnfoctbdjlem  42614  isomennd  42690  smflimlem6  42929  otiunsndisjX  43355  imasetpreimafvbijlemf1  43441  iccpartgt  43464  icceuelpart  43473  ichnreuop  43511  sprsymrelfolem2  43532  sprsymrelf  43534  prproropf1o  43546  reupr  43561  reuopreuprim  43565  isomuspgrlem2c  43872  isomuspgr  43876  ismgmd  43920  mgmhmpropd  43929  mgmhmf1o  43931  idmgmhm  43932  issubmgm2  43934  rabsubmgmd  43935  resmgmhm  43942  resmgmhm2  43943  resmgmhm2b  43944  mgmhmco  43945  submgmacs  43948  opmpoismgm  43951  mgmplusgiopALT  44029  isrnghm2d  44100  c0mgm  44108  c0mhm  44109  lidlmmgm  44124  2zlidl  44133  rnghmsscmap2  44172  rnghmsscmap  44173  rnghmsubcsetclem2  44175  rhmsscmap2  44218  rhmsscmap  44219  rhmsubcsetclem2  44221  rhmsscrnghm  44225  rhmsubcrngclem2  44227  srhmsubc  44275  fldhmsubc  44283  rhmsubc  44289  srhmsubcALTV  44293  fldhmsubcALTV  44301  rhmsubcALTV  44307  lindslinindsimp1  44440
  Copyright terms: Public domain W3C validator