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

Theorem ralrimi 3220
Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.) Shortened after introduction of hbralrimi 3184. (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 2187 . 2 (𝜑 → ∀𝑥𝜑)
3 ralrimi.2 . 2 (𝜑 → (𝑥𝐴𝜓))
42, 3hbralrimi 3184 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1777  wcel 2107  wral 3142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-12 2169
This theorem depends on definitions:  df-bi 208  df-ex 1774  df-nf 1778  df-ral 3147
This theorem is referenced by:  ralimdaa  3221  reximdai  3315  rexlimd2  3320  r19.12  3328  r19.12OLD  3331  r19.37  3347  ralcom2w  3367  ralcom2  3368  rabbida  3479  2rmorex  3748  iineq2d  4938  disjxiun  5059  mpteq2da  5156  fnmptd  6485  mpteqb  6782  fmptdf  6876  eusvobj2  7144  offval2f  7414  zfrep6  7650  wfrlem4  7952  tfr3  8029  tz7.49  8075  mapxpen  8675  dfac2b  9548  hsmexlem4  9843  axcc3  9852  domtriomlem  9856  axdc3lem2  9865  axdc3lem4  9867  axdc4lem  9869  ac6num  9893  dedekind  10795  dedekindle  10796  fsuppmapnn0fiublem  13351  fsuppmapnn0fiub  13352  fprodcllemf  15304  lcmfunsnlem1  15973  lcmfunsnlem2lem1  15974  lcmfunsnlem2  15976  mreexexd  16911  cpmatmcllem  21242  ptcnplem  22145  xkocnv  22338  cfilucfil  23084  itg2splitlem  24264  itg2split  24265  itgeq1f  24287  mptelee  26595  lfgrnloop  26824  foresf1o  30179  funimass4f  30297  fcomptf  30318  aciunf1lem  30322  funcnvmpt  30327  fnpreimac  30331  isarchiofld  30804  reff  30989  locfinreflem  30990  prodindf  31168  esumeq12dvaf  31176  esumgsum  31190  esumel  31192  esumf1o  31195  esumc  31196  esummono  31199  gsumesum  31204  esumlub  31205  esumlef  31207  esumfsup  31215  esumpinfval  31218  esumpinfsum  31222  esum2d  31238  ldsysgenld  31305  sigapildsyslem  31306  ldgenpisyslem1  31308  measinblem  31365  voliune  31374  volmeas  31376  oms0  31441  omssubadd  31444  dstrvprob  31615  bnj1379  31988  bnj1204  32168  bnj1388  32189  bnj1417  32197  bnj1489  32212  untsucf  32820  trpredmintr  32954  frrlem4  33010  domalom  34554  fvineqsneq  34562  cover2  34857  upixp  34872  indexdom  34877  filbcmb  34883  sdclem2  34885  eq0rabdioph  39234  eqrabdioph  39235  setindtr  39482  ss2iundf  39865  gneispace  40345  mnuprdlem3  40471  iunconnlem2  41130  rzalf  41135  fnchoice  41147  refsumcn  41148  rfcnnnub  41154  refsum2cnlem1  41155  iuneq2df  41169  uzwo4  41176  ixpeq2d  41191  ixpssmapc  41197  elintd  41199  ssdf  41200  ralimralim  41206  nelrnmpt  41209  ixpssixp  41219  ballss3  41220  iinssiin  41256  eliind2  41257  ralrimia  41259  rabssd  41272  fompt  41314  choicefi  41324  iunmapss  41339  iunmapsn  41341  axccdom  41348  mptfnd  41373  ssfiunibd  41437  xralrple2  41483  infxr  41496  xrralrecnnle  41514  xrralrecnnge  41523  supxrunb3  41533  fimaxre4  41535  supxrleubrnmpt  41540  rexabslelem  41553  suprleubrnmpt  41557  uzublem  41565  infxrgelbrnmpt  41591  iooiinicc  41679  iooiinioc  41693  mccl  41740  climsuse  41750  mullimc  41758  mullimcf  41765  limcrecl  41771  limsupre  41783  limcleqr  41786  addlimc  41790  0ellimcdiv  41791  limclner  41793  limsupubuzlem  41854  climinf3  41858  limsupequzmpt2  41860  limsupmnfuzlem  41868  limsupre3uzlem  41877  liminfequzmpt2  41933  cncficcgt0  42032  cncfioobd  42041  cncfcompt2  42043  fprodsubrecnncnvlem  42052  fprodaddrecnncnvlem  42054  dvmptfprodlem  42090  dvnprodlem1  42092  iblsplitf  42116  stoweidlem5  42152  stoweidlem16  42163  stoweidlem18  42165  stoweidlem21  42168  stoweidlem26  42173  stoweidlem27  42174  stoweidlem28  42175  stoweidlem29  42176  stoweidlem31  42178  stoweidlem34  42181  stoweidlem36  42183  stoweidlem41  42188  stoweidlem42  42189  stoweidlem44  42191  stoweidlem45  42192  stoweidlem48  42195  stoweidlem51  42198  stoweidlem55  42202  stoweidlem59  42206  stoweidlem60  42207  stoweidlem62  42209  wallispilem3  42214  stirlinglem5  42225  fourierdlem16  42270  fourierdlem21  42275  fourierdlem22  42276  fourierdlem31  42285  fourierdlem39  42293  fourierdlem68  42321  fourierdlem71  42324  fourierdlem73  42326  fourierdlem77  42330  fourierdlem80  42333  fourierdlem83  42336  fourierdlem87  42340  fourierdlem94  42347  fourierdlem103  42356  fourierdlem104  42357  fourierdlem112  42365  fourierdlem113  42366  etransclem32  42413  subsaliuncllem  42502  sge0revalmpt  42522  sge0fodjrnlem  42560  sge0fsummptf  42580  iundjiun  42604  meadjiun  42610  voliunsge0lem  42616  meaiininclem  42630  omeiunle  42661  hoicvrrex  42700  ovnsubaddlem2  42715  hoissrrn2  42722  hoidmv1lelem1  42735  hoidmvlelem3  42741  ovnhoilem1  42745  hoi2toco  42751  ovnlecvr2  42754  hspdifhsp  42760  hoiqssbllem1  42766  hoiqssbllem3  42768  hspmbllem2  42771  iinhoiicclem  42817  iunhoiioolem  42819  vonioo  42826  vonicc  42829  pimconstlt0  42844  pimconstlt1  42845  pimltpnf  42846  pimiooltgt  42851  pimdecfgtioc  42855  pimincfltioc  42856  pimdecfgtioo  42857  pimincfltioo  42858  preimageiingt  42860  preimaleiinlt  42861  issmfd  42874  issmfdf  42876  sssmf  42877  issmfle  42884  issmfdmpt  42887  issmfgt  42895  issmfled  42896  issmfgtd  42899  smflimlem2  42910  smfmullem4  42931  smfpimcclem  42943  smfsuplem1  42947  smfsupmpt  42951  smfinflem  42953  smfinfmpt  42955  iccelpart  43421  mogoldbb  43778  sbgoldbo  43780  aacllem  44730
  Copyright terms: Public domain W3C validator