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

Theorem ralrimivva 3198
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 414 . 2 (𝜑 → ((𝑥𝐴𝑦𝐵) → 𝜓))
32ralrimivv 3196 1 (𝜑 → ∀𝑥𝐴𝑦𝐵 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  wral 3065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ral 3066
This theorem is referenced by:  disjord  5094  disjxiun  5103  otsndisj  5477  otiunsndisj  5478  swopo  5557  issod  5579  reuop  6246  fcof1  7234  fliftfund  7259  isof1oidb  7270  isof1oopb  7271  soisores  7273  soisoi  7274  isocnv  7276  f1oiso  7297  oveqrspc2v  7385  oprres  7523  caovclg  7547  caovcomg  7550  off  7636  caofrss  7654  caonncan  7659  dmmpog  8008  fnmpoovd  8020  fmpoco  8028  fsplitfpar  8051  poxp  8061  fvmpocurryd  8203  smo11  8311  smoiso2  8316  omsmo  8605  nnasmo  8610  coflton  8618  qsdisj2  8735  eroprf  8755  dom2lem  8933  omxpenlem  9018  xpf1o  9084  unxpdomlem3  9197  fofinf1o  9272  dffi3  9368  supmo  9389  infmo  9432  inf3lem6  9570  cantnf  9630  rankxplim  9816  fseqenlem1  9961  fodomacn  9993  iunfictbso  10051  cofsmo  10206  infpssrlem5  10244  enfin2i  10258  fin23lem23  10263  fin23lem27  10265  fin23lem28  10277  compssiso  10311  ltordlem  11681  cju  12150  axdc4uzlem  13889  seqcaopr2  13945  seqhomo  13956  wrd2ind  14612  cshf1  14699  s3sndisj  14853  s3iunsndisj  14854  climcn2  15476  addcn2  15477  mulcn2  15479  o1of2  15496  isercolllem1  15550  fsum2dlem  15656  fsumcom2  15660  fprodser  15833  fprod2dlem  15864  fprodcom2  15868  isprm6  16591  crth  16651  eulerthlem2  16655  vdwlem12  16865  cshwsdisj  16972  imasaddfnlem  17411  imasvscafn  17420  mreexexd  17529  iscatd  17554  oppccomfpropd  17610  isofn  17659  sectmon  17666  ssctr  17709  ssceq  17710  catsubcat  17726  issubc3  17736  fullsubc  17737  fullresc  17738  isfuncd  17752  idfucl  17768  cofucl  17775  funcres2b  17784  fulloppc  17810  fthoppc  17811  idffth  17821  cofull  17822  cofth  17823  ressffth  17826  setcmon  17974  setcepi  17975  resssetc  17979  resscatc  17996  catciso  17998  fthestrcsetc  18039  fullestrcsetc  18040  embedsetcestrclem  18046  fthsetcestrc  18054  fullsetcestrc  18055  evlfcl  18112  uncfcurf  18129  hofcl  18149  yonedalem3  18170  yonedainv  18171  yonffthlem  18172  yoniso  18175  isdrs2  18196  isposd  18213  pospropd  18217  poslubmo  18301  posglbmo  18302  mgmplusf  18508  issstrmgm  18509  opifismgm  18515  ismndd  18579  mndpropd  18582  issubmnd  18584  mndinvmod  18587  ismhmd  18605  mhmpropd  18609  idmhm  18612  mhmf1o  18613  issubmd  18618  mndissubm  18619  0mhm  18631  resmhm  18632  resmhm2  18633  resmhm2b  18634  mhmco  18635  submacs  18638  prdspjmhm  18640  pwsdiagmhm  18642  pwsco1mhm  18643  pwsco2mhm  18644  gsumwspan  18657  frmdsssubm  18672  frmdup1  18675  grpsubf  18827  dfgrp3  18847  mhmmnd  18870  mhmfmhm  18871  issubg4  18948  grpissubg  18949  isnsg3  18963  nsgacs  18965  0nsg  18972  nsgid  18973  cycsubmcom  18998  isghmd  19018  ghmmhm  19019  idghm  19024  ghmnsgima  19033  ghmnsgpreima  19034  ghmf1  19038  ghmf1o  19039  gaid  19080  subgga  19081  gass  19082  gasubg  19083  cntzsubm  19117  cntrsubgnsg  19122  lactghmga  19188  symgfixf1  19220  odf1  19345  sylow1lem2  19382  sylow2blem2  19404  sylow3lem1  19410  lsmssv  19426  smndlsmidm  19439  pj1eu  19479  efglem  19499  efgtf  19505  efgred  19531  efgredeu  19535  frgpmhm  19548  frgpuptf  19553  frgpuplem  19555  mulgmhm  19607  ghmcmn  19611  invghm  19613  ablnsg  19626  cygabl  19669  gsum2d2lem  19751  gsum2d2  19752  gsumcom2  19753  dprd2d2  19824  ablfaclem2  19866  srgfcl  19928  srgcom4lem  19945  srglmhm  19953  srgrmhm  19954  ringcomlem  20001  isrhm2d  20161  kerf1ghm  20178  issubrg2  20245  subrgint  20247  primefld  20275  islmodd  20331  lmodscaf  20347  lmodprop2d  20387  islssd  20399  islss4  20426  lssacs  20431  lsspropd  20481  islmhmd  20503  lmhmima  20511  lmhmpreima  20512  reslmhm  20516  lspextmo  20520  lsmcl  20547  pj1lmhm  20564  islbs2  20618  issubrngd2  20661  opprdomn  20774  abvn0b  20775  expmhm  20869  nn0srg  20870  prmirredlem  20896  expghm  20899  mulgghm2  20900  domnchr  20938  znf1o  20961  zntoslem  20966  znfld  20970  cygznlem3  20979  phlipf  21059  dsmmlss  21153  uvcf1  21201  frlmlbs  21206  lindff1  21229  lindfrn  21230  f1lindf  21231  issubassa2  21298  mvrf1  21397  mplsubglem  21408  mplsubrg  21414  mplcoe5lem  21443  mplcoe2  21445  mplind  21481  evlslem2  21492  evlseu  21496  mhplss  21548  ply1sclf1  21663  mamucl  21751  mamuass  21752  mamudi  21753  mamudir  21754  mamuvs1  21755  mamuvs2  21756  matbas2d  21775  mamumat1cl  21791  mamulid  21793  mamurid  21794  mat1mhm  21836  dmatid  21847  dmatsubcl  21850  dmatsgrp  21851  dmatmulcl  21852  dmatsrng  21853  dmatcrng  21854  scmatscmiddistr  21860  scmatscm  21865  scmatsgrp  21871  scmatsrng  21872  scmatcrng  21873  scmatsgrp1  21874  scmatsrng1  21875  scmatf1  21883  scmatmhm  21886  mavmul0g  21905  mdet1  21953  mdetunilem9  21972  mdetuni0  21973  mdetmul  21975  madutpos  21994  smadiadetlem4  22021  1elcpmat  22067  cpmatacl  22068  cpmatmcl  22071  mat2pmatf1  22081  mat2pmatmul  22083  mat2pmat1  22084  mat2pmatlin  22087  m2cpm  22093  m2cpminvid  22105  m2cpminvid2  22107  decpmatmul  22124  pmatcollpw1  22128  monmatcollpw  22131  pmatcollpw  22133  pmatcollpw3lem  22135  pmatcollpwscmatlem2  22142  pm2mpf1  22151  mp2pm2mplem4  22161  pm2mpmhmlem2  22171  chp0mat  22198  chpidmat  22199  tgclb  22323  mretopd  22446  toponmre  22447  iscldtop  22449  ordtbaslem  22542  ordtbas2  22545  cnt0  22700  haust1  22706  cnhaus  22708  isreg2  22731  dishaus  22736  ordthaus  22738  dfconn2  22773  iunconn  22782  clsconn  22784  2ndcomap  22812  dis2ndc  22814  llynlly  22831  restnlly  22836  restlly  22837  islly2  22838  llyidm  22842  nllyidm  22843  hausllycmp  22848  kgentopon  22892  txbas  22921  ptbasin2  22932  ptbasfi  22935  txcnp  22974  txcnmpt  22978  pthaus  22992  tx1stc  23004  xkococnlem  23013  xkococn  23014  cnmpt21  23025  qtoptop2  23053  qtopeu  23070  kqt0lem  23090  isr0  23091  regr1lem2  23094  kqreglem1  23095  kqreglem2  23096  kqnrmlem1  23097  kqnrmlem2  23098  nrmr0reg  23103  reghmph  23147  nrmhmph  23148  txswaphmeo  23159  qtophmeo  23171  fbun  23194  trfbas2  23197  isfil2  23210  infil  23217  trfil2  23241  filssufilg  23265  hausflim  23335  fclsnei  23373  fclsfnflim  23381  flimfnfcls  23382  ptcmplem1  23406  clssubg  23463  tgpconncomp  23467  qustgplem  23475  tsmsfbas  23482  utoptop  23589  iducn  23638  cstucnd  23639  isxmetd  23682  isxmet2d  23683  xmettpos  23705  prdsdsf  23723  prdsmet  23726  ressprdsds  23727  imasdsf1olem  23729  imasf1oxmet  23731  imasf1omet  23732  blfvalps  23739  xmetresbl  23793  metss2  23871  comet  23872  stdbdmet  23875  stdbdmopn  23877  methaus  23879  met2ndci  23881  metustfbas  23916  nrmmetd  23933  subgngp  23994  ngptgp  23995  sranlm  24051  nlmvscnlem1  24053  nlmvscn  24054  nrginvrcn  24059  lssnlm  24068  nghmcn  24112  qtopbaslem  24125  reconn  24194  xmetdcn2  24203  metdscn  24222  metnrm  24228  elcncf1di  24261  cncfcdm  24264  mulc1cncf  24271  cncfco  24273  reparphti  24363  isncvsngpd  24517  tcphcph  24604  ipcnlem1  24612  ipcn  24613  iscfil3  24640  bcthlem5  24695  rrxmet  24775  minveclem3  24796  minveclem7  24802  ovolicc2lem4  24887  dyadmbl  24967  volcn  24973  itg1addlem1  25059  itg1addlem2  25064  itg1addlem4  25066  itg1addlem4OLD  25067  mbfi1fseqlem1  25083  mbfi1fseqlem3  25085  mbfi1fseqlem4  25086  mbfi1fseqlem5  25087  dvmptfsum  25342  c1liplem1  25363  dvgt0lem2  25370  ftc1a  25404  ply1domn  25491  ply1divmo  25503  fta1b  25537  ig1peu  25539  coeeu  25589  plydivalg  25662  aaliou2b  25704  ulmss  25759  ulmcn  25761  efif1olem4  25904  efsubm  25910  logccv  26021  logbmpt  26141  logbfval  26143  cvxcl  26337  basellem4  26436  fsumdvdscom  26537  musum  26543  dvdsmulf1o  26546  fsumdvdsmul  26547  dchrelbasd  26590  dchrmulcl  26600  dchrinv  26612  lgsqrlem2  26698  lgsdchr  26706  lgseisenlem2  26727  lgsquadlem1  26731  lgsquadlem2  26732  2sqreulem4  26805  dchrisumlema  26839  dchrisumlem2  26841  chpdifbndlem2  26905  pntpbnd  26939  pntibndlem3  26943  ssltd  27134  oldbday  27233  addsprop  27291  axtgcont  27414  tgjustc1  27420  tgjustc2  27421  iscgrglt  27459  ercgrg  27462  idmot  27482  motco  27485  cnvmot  27486  motcgrg  27489  tgisline  27572  tghilberti2  27583  mirreu3  27599  mirmot  27620  ragperp  27662  foot  27667  mideu  27683  midf  27721  lmimot  27743  trgcopyeu  27751  f1otrgds  27814  f1otrg  27816  f1otrge  27817  xmstrkgc  27837  brbtwn2  27857  axlowdimlem15  27908  axcontlem2  27917  axcontlem10  27925  eengtrkg  27938  eengtrkge  27939  numedglnl  28098  usgredgreu  28169  uspgredg2vtxeu  28171  uspgredg2v  28175  usgredg2v  28178  wlkswwlksf1o  28827  wwlksnextinj  28847  clwlkclwwlkf1  28957  clwwlkf1  28996  frcond4  29217  frgrncvvdeqlem8  29253  frgrncvvdeq  29256  frgrwopreglem4  29262  numclwwlk1lem2f1  29304  grpoinvf  29477  nvmf  29590  vacn  29639  nmcvcn  29640  smcnlem  29642  sspg  29673  ssps  29675  sspmlem  29677  0lno  29735  blocni  29750  ipblnfi  29800  minvecolem7  29828  unopf1o  30861  cnvunop  30863  unoplin  30865  counop  30866  hmopadj2  30886  hmoplin  30887  bralnfn  30893  lnopeq0i  30952  hmops  30965  hmopm  30966  hmopco  30968  lnconi  30978  cnlnadjlem2  31013  adjmul  31037  adjadd  31038  cdjreui  31377  disjxpin  31509  off2  31560  2ndresdju  31568  fnpreimac  31590  suppovss  31601  f1od2  31641  xrofsup  31675  s3f1  31806  ccatf1  31808  swrdf1  31813  odutos  31831  dfmgc2lem  31858  dfmgc2  31859  pwrssmgc  31863  mgcf1o  31866  abliso  31890  symgcntz  31939  tocyccntz  31996  archiabllem1  32032  archiabllem2  32036  suborng  32113  xrge0slmod  32143  nsgmgc  32193  intlidl  32202  rhmpreimaidl  32203  idlinsubrg  32208  rhmimaidl  32209  prmidl2  32216  idlmulssprm  32217  isprmidlc  32223  rhmpreimaprmidl  32227  qsidomlem1  32228  qsidomlem2  32229  mxidlprm  32240  ssmxidllem  32241  lindsun  32323  fedgmullem1  32327  fedgmullem2  32328  fedgmul  32329  1smat1  32388  submateq  32393  madjusmdetlem3  32413  zart0  32463  pstmxmet  32481  ofcf  32705  ldgenpisys  32768  rossros  32782  inelcarsg  32914  sibfof  32943  sitmf  32955  hgt750lemb  33272  erdszelem4  33791  erdszelem9  33796  erdsze2lem2  33801  cnpconn  33827  pconnconn  33828  txpconn  33829  ptpconn  33830  cvxpconn  33839  cvxsconn  33840  iccllysconn  33847  cvmseu  33873  cvmliftmo  33881  cvmlift2lem5  33904  cvmlift2lem9  33908  mrsubff1  34111  elmrsubrn  34117  mrsubco  34118  msubff1  34153  mvhf1  34156  segconeu  34599  fnessref  34832  neibastop1  34834  filnetlem3  34855  onsuct0  34916  unblimceq0lem  34972  unbdqndv2  34977  knoppndv  35000  irrdiff  35800  uncf  36060  fin2so  36068  lindsadd  36074  poimirlem4  36085  poimirlem13  36094  poimirlem14  36095  poimirlem26  36107  heicant  36116  mblfinlem2  36119  ftc1anc  36162  sdclem1  36205  isbnd3  36246  prdsbnd  36255  ismtycnv  36264  ismtyhmeolem  36266  ismtyres  36270  bfplem1  36284  bfplem2  36285  bfp  36286  rrnmet  36291  ismrer1  36300  iccbnd  36302  grpokerinj  36355  isdrngo2  36420  rngogrphom  36433  rngohomco  36436  rngoisocnv  36443  iscringd  36460  eqvreldisj1  37289  erprt  37338  lfl0f  37534  lkrlss  37560  lshpsmreu  37574  linepsubN  38218  pmapsub  38234  lautcnv  38556  lautco  38563  idltrn  38616  cdleme50f1  39009  cdleme50laut  39013  istendod  39228  dihf11  39733  dih1dimatlem  39795  lcfl7N  39967  lcfrlem9  40016  mapd1o  40114  hdmapf1oN  40331  hgmapf1oN  40369  qsalrel  40667  imacrhmcl  40698  fsuppind  40768  sn-negex12  40888  nacsfix  41038  rmxypairf1o  41238  wepwsolem  41372  dnnumch3  41377  fnwe2  41383  mpaaeu  41480  idomsubgmo  41528  mon1psubm  41536  deg1mhm  41537  isotone1  42327  isotone2  42328  mnringmulrcld  42515  disjxp1  43284  disjf1  43408  wessf1ornlem  43410  projf1o  43424  sumnnodd  43878  lptioo2  43879  lptioo1  43880  cncfshift  44122  cncfperiod  44127  dvnprodlem1  44194  fourierdlem42  44397  nnfoctbdjlem  44703  isomennd  44779  smflimlem6  45024  fsetsnf1  45293  cfsetsnfsetf1  45300  otiunsndisjX  45518  imasetpreimafvbijlemf1  45603  iccpartgt  45626  icceuelpart  45635  ichnreuop  45671  sprsymrelfolem2  45692  sprsymrelf  45694  prproropf1o  45706  reupr  45721  reuopreuprim  45725  isomuspgrlem2c  46029  isomuspgr  46033  ismgmd  46077  mgmhmpropd  46086  mgmhmf1o  46088  idmgmhm  46089  issubmgm2  46091  rabsubmgmd  46092  resmgmhm  46099  resmgmhm2  46100  resmgmhm2b  46101  mgmhmco  46102  submgmacs  46105  opmpoismgm  46108  mgmplusgiopALT  46135  isrnghm2d  46206  c0mgm  46214  c0mhm  46215  lidlmmgm  46230  2zlidl  46239  rnghmsscmap2  46278  rnghmsscmap  46279  rnghmsubcsetclem2  46281  rhmsscmap2  46324  rhmsscmap  46325  rhmsubcsetclem2  46327  rhmsscrnghm  46331  rhmsubcrngclem2  46333  srhmsubc  46381  fldhmsubc  46389  rhmsubc  46395  srhmsubcALTV  46399  fldhmsubcALTV  46407  rhmsubcALTV  46413  lindslinindsimp1  46545  1arymaptf1  46735  2arymaptf1  46746  toslat  47014  catprsc  47040  catprsc2  47041  isthincd  47064  isthincd2  47065  functhinclem4  47071  thincfth  47075  thincciso  47076
  Copyright terms: Public domain W3C validator