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

Theorem ralrimi 3145
Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (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 2230 . 2 (𝜑 → ∀𝑥𝜑)
3 ralrimi.2 . 2 (𝜑 → (𝑥𝐴𝜓))
42, 3hbralrimi 3142 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1863  wcel 2156  wral 3096
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-12 2214
This theorem depends on definitions:  df-bi 198  df-ex 1860  df-nf 1864  df-ral 3101
This theorem is referenced by:  ralimdaa  3146  reximdai  3199  rexlimd2  3213  r19.12  3251  r19.37  3274  ralcom2  3292  2rmorex  3610  iineq2d  4733  disjxiun  4841  mpteq2da  4937  mpteqb  6516  fmptdf  6605  eusvobj2  6863  offval2f  7135  zfrep6  7360  wfrlem4  7649  wfrlem4OLD  7650  tfr3  7727  tz7.49  7772  mapxpen  8361  dfac2b  9232  dfac2OLD  9234  hsmexlem4  9532  axcc3  9541  domtriomlem  9545  axdc3lem2  9554  axdc3lem4  9556  axdc4lem  9558  ac6num  9582  dedekind  10481  dedekindle  10482  fsuppmapnn0fiublem  13009  fsuppmapnn0fiub  13010  fprodcllemf  14905  lcmfunsnlem1  15565  lcmfunsnlem2lem1  15566  lcmfunsnlem2  15568  mreexexd  16509  cpmatmcllem  20732  ptcnplem  21634  xkocnv  21827  cfilucfil  22573  itg2splitlem  23725  itg2split  23726  itgeq1f  23748  mptelee  25985  lfgrnloop  26230  foresf1o  29664  funimass4f  29760  fcomptf  29781  aciunf1lem  29785  funcnvmptOLD  29790  funcnvmpt  29791  isarchiofld  30138  reff  30227  locfinreflem  30228  prodindf  30406  esumeq12dvaf  30414  esumgsum  30428  esumel  30430  esumf1o  30433  esumc  30434  esummono  30437  gsumesum  30442  esumlub  30443  esumlef  30445  esumfsup  30453  esumpinfval  30456  esumpinfsum  30460  esum2d  30476  ldsysgenld  30544  sigapildsyslem  30545  ldgenpisyslem1  30547  measinblem  30604  voliune  30613  volmeas  30615  oms0  30680  omssubadd  30683  dstrvprob  30854  bnj1379  31219  bnj1204  31398  bnj1388  31419  bnj1417  31427  bnj1489  31442  untsucf  31904  trpredmintr  32046  frrlem4  32099  bj-rabbida  33219  cover2  33815  upixp  33831  indexdom  33836  filbcmb  33842  sdclem2  33844  eq0rabdioph  37836  eqrabdioph  37837  setindtr  38086  ss2iundf  38445  gneispace  38926  iunconnlem2  39659  rzalf  39664  fnchoice  39676  refsumcn  39677  rfcnnnub  39683  refsum2cnlem1  39684  iuneq2df  39699  uzwo4  39708  ixpeq2d  39724  ixpssmapc  39730  elintd  39732  ssdf  39734  ralimralim  39740  nelrnmpt  39744  ixpssixp  39756  ballss3  39757  rabbida  39761  iinssiin  39797  eliind2  39798  ralrimia  39800  rabssd  39816  fompt  39862  rnmptssd  39868  choicefi  39873  iunmapss  39888  iunmapsn  39890  rnmpt0  39893  axccdom  39897  dmmptdf  39898  axccd  39907  fnmptd  39912  dmmptdf2  39917  mptfnd  39929  mpteq12da  39930  rnmptbd2lem  39940  rnmptssdf  39946  rnmptbdlem  39947  ssfiunibd  39998  xralrple2  40044  infxr  40057  xrralrecnnle  40076  xrralrecnnge  40086  supxrunb3  40096  fimaxre4  40098  supxrleubrnmpt  40105  rexabslelem  40118  suprleubrnmpt  40122  uzublem  40130  infxrgelbrnmpt  40156  iooiinicc  40243  iooiinioc  40257  mccl  40304  climsuse  40314  mullimc  40322  mullimcf  40329  limcrecl  40335  limsupre  40347  limcleqr  40350  addlimc  40354  0ellimcdiv  40355  limclner  40357  limsupubuzlem  40418  climinf3  40422  limsupequzmpt2  40424  limsupmnfuzlem  40432  limsupre3uzlem  40441  liminfequzmpt2  40497  cncficcgt0  40575  cncfioobd  40584  cncfcompt2  40586  fprodsubrecnncnvlem  40595  fprodaddrecnncnvlem  40597  dvmptfprodlem  40633  dvnprodlem1  40635  iblsplitf  40659  stoweidlem5  40695  stoweidlem16  40706  stoweidlem18  40708  stoweidlem21  40711  stoweidlem26  40716  stoweidlem27  40717  stoweidlem28  40718  stoweidlem29  40719  stoweidlem31  40721  stoweidlem34  40724  stoweidlem36  40726  stoweidlem41  40731  stoweidlem42  40732  stoweidlem44  40734  stoweidlem45  40735  stoweidlem48  40738  stoweidlem51  40741  stoweidlem55  40745  stoweidlem59  40749  stoweidlem60  40750  stoweidlem62  40752  wallispilem3  40757  stirlinglem5  40768  fourierdlem16  40813  fourierdlem21  40818  fourierdlem22  40819  fourierdlem31  40828  fourierdlem39  40836  fourierdlem68  40864  fourierdlem71  40867  fourierdlem73  40869  fourierdlem77  40873  fourierdlem80  40876  fourierdlem83  40879  fourierdlem87  40883  fourierdlem94  40890  fourierdlem103  40899  fourierdlem104  40900  fourierdlem112  40908  fourierdlem113  40909  etransclem32  40956  subsaliuncllem  41048  sge0revalmpt  41068  sge0fodjrnlem  41106  sge0fsummptf  41126  iundjiun  41150  meadjiun  41156  voliunsge0lem  41162  meaiininclem  41176  omeiunle  41207  hoicvrrex  41246  ovnsubaddlem2  41261  hoissrrn2  41268  hoidmv1lelem1  41281  hoidmvlelem3  41287  ovnhoilem1  41291  hoi2toco  41297  ovnlecvr2  41300  hspdifhsp  41306  hoiqssbllem1  41312  hoiqssbllem3  41314  hspmbllem2  41317  iinhoiicclem  41363  iunhoiioolem  41365  vonioo  41372  vonicc  41375  pimconstlt0  41390  pimconstlt1  41391  pimltpnf  41392  pimiooltgt  41397  pimdecfgtioc  41401  pimincfltioc  41402  pimdecfgtioo  41403  pimincfltioo  41404  preimageiingt  41406  preimaleiinlt  41407  issmfd  41420  issmfdf  41422  sssmf  41423  issmfle  41430  issmfdmpt  41433  issmfgt  41441  issmfled  41442  issmfgtd  41445  smflimlem2  41456  smfmullem4  41477  smfpimcclem  41489  smfsuplem1  41493  smfsupmpt  41497  smfinflem  41499  smfinfmpt  41501  iccelpart  41938  mogoldbb  42242  sbgoldbo  42244  aacllem  43112
  Copyright terms: Public domain W3C validator