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

Theorem ralrimi 3243
Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). For a version based on fewer axioms see ralrimiv 3143. (Contributed by NM, 10-Oct-1999.) Shortened after introduction of hbralrimi 3142. (Revised by Wolf Lammen, 4-Dec-2019.)
Hypotheses
Ref Expression
ralrimi.1 𝑥𝜑
ralrimi.2 (𝜑 → (𝑥𝐴𝜓))
Assertion
Ref Expression
ralrimi (𝜑 → ∀𝑥𝐴 𝜓)

Proof of Theorem ralrimi
StepHypRef Expression
1 ralrimi.1 . . 3 𝑥𝜑
21nf5ri 2189 . 2 (𝜑 → ∀𝑥𝜑)
3 ralrimi.2 . 2 (𝜑 → (𝑥𝐴𝜓))
42, 3hbralrimi 3142 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1786  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  ax-6 1972  ax-7 2012  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787  df-ral 3066
This theorem is referenced by:  ralrimia  3244  ralimdaa  3246  reximdai  3247  r19.37  3248  rexlimd2  3251  r19.12  3300  r19.12OLD  3301  ralcom2  3353  rabbida  3436  2rmorex  3717  iineq2d  4982  disjxiun  5107  mpteq2daOLD  5209  rnmpt0f  6200  fnmptd  6647  mpteqb  6972  fmptdf  7070  eusvobj2  7354  offval2f  7637  zfrep6  7892  frrlem4  8225  wfrlem4OLD  8263  tfr3  8350  tz7.49  8396  mapxpen  9094  dfac2b  10073  hsmexlem4  10372  axcc3  10381  domtriomlem  10385  axdc3lem2  10394  axdc3lem4  10396  axdc4lem  10398  ac6num  10422  dedekind  11325  dedekindle  11326  fsuppmapnn0fiublem  13902  fsuppmapnn0fiub  13903  fprodcllemf  15848  lcmfunsnlem1  16520  lcmfunsnlem2lem1  16521  lcmfunsnlem2  16523  mreexexd  17535  cpmatmcllem  22083  ptcnplem  22988  xkocnv  23181  cfilucfil  23931  cncfcompt2  24287  itg2splitlem  25129  itg2split  25130  itgeq1f  25152  mptelee  27886  lfgrnloop  28118  foresf1o  31473  iinabrex  31529  funimass4f  31593  fcomptf  31616  aciunf1lem  31620  funcnvmpt  31625  fnpreimac  31629  isarchiofld  32152  reff  32460  locfinreflem  32461  zarclsiin  32492  zarcmplem  32502  prodindf  32662  esumeq12dvaf  32670  esumgsum  32684  esumel  32686  esumf1o  32689  esumc  32690  esummono  32693  gsumesum  32698  esumlub  32699  esumlef  32701  esumfsup  32709  esumpinfval  32712  esumpinfsum  32716  esum2d  32732  ldsysgenld  32799  sigapildsyslem  32800  ldgenpisyslem1  32802  measinblem  32859  voliune  32868  volmeas  32870  oms0  32937  omssubadd  32940  dstrvprob  33111  bnj1379  33482  bnj1204  33664  bnj1388  33685  bnj1417  33693  bnj1489  33708  untsucf  34321  domalom  35904  fvineqsneq  35912  cover2  36202  upixp  36217  indexdom  36222  filbcmb  36228  sdclem2  36230  eq0rabdioph  41128  eqrabdioph  41129  setindtr  41377  gneispace  42480  mnuprdlem3  42628  iunconnlem2  43291  rzalf  43296  fnchoice  43308  refsumcn  43309  rfcnnnub  43315  refsum2cnlem1  43316  iuneq2df  43328  uzwo4  43335  ixpeq2d  43350  ixpssmapc  43356  elintd  43358  ssdf  43359  ralimralim  43365  nelrnmpt  43368  ixpssixp  43376  ballss3  43377  iinssiin  43413  eliind2  43414  rabssd  43426  ss2rabdf  43439  fompt  43485  choicefi  43495  iunmapss  43510  iunmapsn  43512  axccdom  43517  mptfnd  43542  ssfiunibd  43617  xralrple2  43662  infxr  43675  xrralrecnnle  43691  xrralrecnnge  43699  supxrunb3  43708  fimaxre4  43710  supxrleubrnmpt  43715  rexabslelem  43727  suprleubrnmpt  43731  uzublem  43739  infxrgelbrnmpt  43763  iooiinicc  43854  iooiinioc  43868  mccl  43913  climsuse  43923  mullimc  43931  mullimcf  43938  limcrecl  43944  limsupre  43956  limcleqr  43959  addlimc  43963  0ellimcdiv  43964  limclner  43966  limsupubuzlem  44027  climinf3  44031  limsupequzmpt2  44033  limsupmnfuzlem  44041  limsupre3uzlem  44050  liminfequzmpt2  44106  cncficcgt0  44203  cncfioobd  44212  fprodsubrecnncnvlem  44222  fprodaddrecnncnvlem  44224  dvmptfprodlem  44259  dvnprodlem1  44261  iblsplitf  44285  stoweidlem5  44320  stoweidlem16  44331  stoweidlem18  44333  stoweidlem21  44336  stoweidlem26  44341  stoweidlem27  44342  stoweidlem28  44343  stoweidlem29  44344  stoweidlem31  44346  stoweidlem34  44349  stoweidlem36  44351  stoweidlem41  44356  stoweidlem42  44357  stoweidlem44  44359  stoweidlem45  44360  stoweidlem48  44363  stoweidlem51  44366  stoweidlem55  44370  stoweidlem59  44374  stoweidlem60  44375  stoweidlem62  44377  wallispilem3  44382  stirlinglem5  44393  fourierdlem16  44438  fourierdlem21  44443  fourierdlem22  44444  fourierdlem31  44453  fourierdlem39  44461  fourierdlem68  44489  fourierdlem71  44492  fourierdlem73  44494  fourierdlem77  44498  fourierdlem80  44501  fourierdlem83  44504  fourierdlem87  44508  fourierdlem94  44515  fourierdlem103  44524  fourierdlem104  44525  fourierdlem112  44533  fourierdlem113  44534  etransclem32  44581  subsaliuncllem  44672  sge0revalmpt  44693  sge0fodjrnlem  44731  sge0fsummptf  44751  iundjiun  44775  meadjiun  44781  voliunsge0lem  44787  meaiininclem  44801  omeiunle  44832  hoicvrrex  44871  ovnsubaddlem2  44886  hoissrrn2  44893  hoidmv1lelem1  44906  hoidmvlelem3  44912  ovnhoilem1  44916  hoi2toco  44922  ovnlecvr2  44925  hspdifhsp  44931  hoiqssbllem1  44937  hoiqssbllem3  44939  hspmbllem2  44942  iinhoiicclem  44988  iunhoiioolem  44990  vonioo  44997  vonicc  45000  pimconstlt0  45016  pimconstlt1  45017  pimltpnff  45018  pimiooltgt  45025  pimdecfgtioc  45030  pimincfltioc  45031  pimdecfgtioo  45032  pimincfltioo  45033  preimageiingt  45035  preimaleiinlt  45036  pimgtmnff  45037  issmfd  45050  issmfdf  45052  sssmf  45053  issmfle  45060  issmfdmpt  45063  issmfgt  45071  issmfled  45072  issmfgtd  45076  smflimlem2  45087  smfmullem4  45109  smfpimcclem  45122  smfsuplem1  45126  smfinflem  45132  smfinfmpt  45134  iccelpart  45699  mogoldbb  46051  sbgoldbo  46053  pgindnf  47235  aacllem  47322
  Copyright terms: Public domain W3C validator