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

Theorem ralrimi 2986
 Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.) Shortened after introduction of hbralrimi 2983. (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 2103 . 2 (𝜑 → ∀𝑥𝜑)
3 ralrimi.2 . 2 (𝜑 → (𝑥𝐴𝜓))
42, 3hbralrimi 2983 1 (𝜑 → ∀𝑥𝐴 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  Ⅎwnf 1748   ∈ wcel 2030  ∀wral 2941 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087 This theorem depends on definitions:  df-bi 197  df-ex 1745  df-nf 1750  df-ral 2946 This theorem is referenced by:  ralimdaa  2987  reximdai  3041  rexlimd2  3054  r19.12  3092  r19.37  3115  ralcom2  3133  2rmorex  3445  iineq2d  4573  disjxiun  4681  disjxiunOLD  4682  mpteq2da  4776  mpteqb  6338  fmptdf  6427  eusvobj2  6683  offval2f  6951  zfrep6  7176  wfrlem4  7463  tfr3  7540  tz7.49  7585  mapxpen  8167  dfac2  8991  hsmexlem4  9289  axcc3  9298  domtriomlem  9302  axdc3lem2  9311  axdc3lem4  9313  axdc4lem  9315  ac6num  9339  dedekind  10238  dedekindle  10239  fsuppmapnn0fiublem  12829  fsuppmapnn0fiub  12830  fsuppmapnn0fiubOLD  12831  fprodcllemf  14732  lcmfunsnlem1  15397  lcmfunsnlem2lem1  15398  lcmfunsnlem2  15400  mreexexd  16355  mreexexdOLD  16356  cpmatmcllem  20571  ptcnplem  21472  xkocnv  21665  cfilucfil  22411  itg2splitlem  23560  itg2split  23561  itgeq1f  23583  mptelee  25820  lfgrnloop  26065  foresf1o  29469  funimass4f  29565  fcomptf  29586  aciunf1lem  29590  funcnvmptOLD  29595  funcnvmpt  29596  isarchiofld  29945  reff  30034  locfinreflem  30035  prodindf  30213  esumeq12dvaf  30221  esumgsum  30235  esumel  30237  esumf1o  30240  esumc  30241  esummono  30244  gsumesum  30249  esumlub  30250  esumlef  30252  esumfsup  30260  esumpinfval  30263  esumpinfsum  30267  esum2d  30283  ldsysgenld  30351  sigapildsyslem  30352  ldgenpisyslem1  30354  measinblem  30411  voliune  30420  volmeas  30422  oms0  30487  omssubadd  30490  dstrvprob  30661  bnj1379  31027  bnj1204  31206  bnj1388  31227  bnj1417  31235  bnj1489  31250  untsucf  31713  trpredmintr  31855  frrlem4  31908  bj-rabbida  33039  cover2  33638  upixp  33654  indexdom  33659  filbcmb  33665  sdclem2  33668  eq0rabdioph  37657  eqrabdioph  37658  setindtr  37908  ss2iundf  38268  gneispace  38749  iunconnlem2  39485  rzalf  39490  fnchoice  39502  refsumcn  39503  rfcnnnub  39509  refsum2cnlem1  39510  iuneq2df  39526  uzwo4  39535  ixpeq2d  39551  ixpssmapc  39557  elintd  39559  ssdf  39561  ralimralim  39567  nelrnmpt  39571  ixpssixp  39583  ballss3  39584  rabbida  39588  iinssiin  39626  eliind2  39627  ralrimia  39629  rabssd  39646  fompt  39693  rnmptssd  39699  choicefi  39706  iunmapss  39721  iunmapsn  39723  rnmpt0  39726  axccdom  39730  dmmptdf  39731  axccd  39743  fnmptd  39748  dmmptdf2  39753  mptfnd  39765  mpteq12da  39766  rnmptbd2lem  39777  rnmptssdf  39783  rnmptbdlem  39784  ssfiunibd  39837  xralrple2  39883  infxr  39896  xrralrecnnle  39915  xrralrecnnge  39926  supxrunb3  39936  fimaxre4  39938  supxrleubrnmpt  39945  rexabslelem  39958  suprleubrnmpt  39962  uzublem  39970  infxrgelbrnmpt  39996  iooiinicc  40087  iooiinioc  40101  mccl  40148  climsuse  40158  mullimc  40166  mullimcf  40173  limcrecl  40179  limsupre  40191  limcleqr  40194  addlimc  40198  0ellimcdiv  40199  limclner  40201  limsupubuzlem  40262  climinf3  40266  limsupequzmpt2  40268  limsupmnfuzlem  40276  limsupre3uzlem  40285  liminfequzmpt2  40341  cncficcgt0  40419  cncfioobd  40428  cncfcompt2  40430  fprodsubrecnncnvlem  40439  fprodaddrecnncnvlem  40441  dvmptfprodlem  40477  dvnprodlem1  40479  iblsplitf  40504  stoweidlem5  40540  stoweidlem16  40551  stoweidlem18  40553  stoweidlem21  40556  stoweidlem26  40561  stoweidlem27  40562  stoweidlem28  40563  stoweidlem29  40564  stoweidlem31  40566  stoweidlem34  40569  stoweidlem36  40571  stoweidlem41  40576  stoweidlem42  40577  stoweidlem44  40579  stoweidlem45  40580  stoweidlem48  40583  stoweidlem51  40586  stoweidlem55  40590  stoweidlem59  40594  stoweidlem60  40595  stoweidlem62  40597  wallispilem3  40602  stirlinglem5  40613  fourierdlem16  40658  fourierdlem21  40663  fourierdlem22  40664  fourierdlem31  40673  fourierdlem39  40681  fourierdlem68  40709  fourierdlem71  40712  fourierdlem73  40714  fourierdlem77  40718  fourierdlem80  40721  fourierdlem83  40724  fourierdlem87  40728  fourierdlem94  40735  fourierdlem103  40744  fourierdlem104  40745  fourierdlem112  40753  fourierdlem113  40754  etransclem32  40801  subsaliuncllem  40893  sge0revalmpt  40913  sge0fodjrnlem  40951  sge0fsummptf  40971  iundjiun  40995  meadjiun  41001  voliunsge0lem  41007  meaiininclem  41021  omeiunle  41052  hoicvrrex  41091  ovnsubaddlem2  41106  hoissrrn2  41113  hoidmv1lelem1  41126  hoidmvlelem3  41132  ovnhoilem1  41136  hoi2toco  41142  ovnlecvr2  41145  hspdifhsp  41151  hoiqssbllem1  41157  hoiqssbllem3  41159  hspmbllem2  41162  iinhoiicclem  41208  iunhoiioolem  41210  vonioo  41217  vonicc  41220  pimconstlt0  41235  pimconstlt1  41236  pimltpnf  41237  pimiooltgt  41242  pimdecfgtioc  41246  pimincfltioc  41247  pimdecfgtioo  41248  pimincfltioo  41249  preimageiingt  41251  preimaleiinlt  41252  issmfd  41265  issmfdf  41267  sssmf  41268  issmfle  41275  issmfdmpt  41278  issmfgt  41286  issmfled  41287  issmfgtd  41290  smflimlem2  41301  smfmullem4  41322  smfpimcclem  41334  smfsuplem1  41338  smfsupmpt  41342  smfinflem  41344  smfinfmpt  41346  iccelpart  41694  mogoldbb  41998  sbgoldbo  42000  aacllem  42875
 Copyright terms: Public domain W3C validator