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

Theorem ralrimi 3180
 Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.) Shortened after introduction of hbralrimi 3147. (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 2193 . 2 (𝜑 → ∀𝑥𝜑)
3 ralrimi.2 . 2 (𝜑 → (𝑥𝐴𝜓))
42, 3hbralrimi 3147 1 (𝜑 → ∀𝑥𝐴 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  Ⅎwnf 1785   ∈ wcel 2111  ∀wral 3106 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175 This theorem depends on definitions:  df-bi 210  df-ex 1782  df-nf 1786  df-ral 3111 This theorem is referenced by:  ralimdaa  3181  reximdai  3270  rexlimd2  3275  r19.12  3283  r19.37  3297  ralcom2  3316  rabbida  3421  2rmorex  3693  iineq2d  4905  disjxiun  5028  mpteq2da  5125  fnmptd  6462  mpteqb  6765  fmptdf  6859  eusvobj2  7129  offval2f  7404  zfrep6  7641  wfrlem4  7944  tfr3  8021  tz7.49  8067  mapxpen  8670  dfac2b  9544  hsmexlem4  9843  axcc3  9852  domtriomlem  9856  axdc3lem2  9865  axdc3lem4  9867  axdc4lem  9869  ac6num  9893  dedekind  10795  dedekindle  10796  fsuppmapnn0fiublem  13356  fsuppmapnn0fiub  13357  fprodcllemf  15307  lcmfunsnlem1  15974  lcmfunsnlem2lem1  15975  lcmfunsnlem2  15977  mreexexd  16914  cpmatmcllem  21333  ptcnplem  22236  xkocnv  22429  cfilucfil  23176  cncfcompt2  23523  itg2splitlem  24362  itg2split  24363  itgeq1f  24385  mptelee  26699  lfgrnloop  26928  foresf1o  30283  iinabrex  30342  funimass4f  30406  fcomptf  30431  aciunf1lem  30435  funcnvmpt  30440  fnpreimac  30444  isarchiofld  30951  reff  31207  locfinreflem  31208  zarclsiin  31239  zarcmplem  31249  prodindf  31407  esumeq12dvaf  31415  esumgsum  31429  esumel  31431  esumf1o  31434  esumc  31435  esummono  31438  gsumesum  31443  esumlub  31444  esumlef  31446  esumfsup  31454  esumpinfval  31457  esumpinfsum  31461  esum2d  31477  ldsysgenld  31544  sigapildsyslem  31545  ldgenpisyslem1  31547  measinblem  31604  voliune  31613  volmeas  31615  oms0  31680  omssubadd  31683  dstrvprob  31854  bnj1379  32227  bnj1204  32409  bnj1388  32430  bnj1417  32438  bnj1489  32453  untsucf  33064  trpredmintr  33198  frrlem4  33254  domalom  34840  fvineqsneq  34848  cover2  35171  upixp  35186  indexdom  35191  filbcmb  35197  sdclem2  35199  eq0rabdioph  39760  eqrabdioph  39761  setindtr  40008  ss2iundf  40403  gneispace  40880  mnuprdlem3  41025  iunconnlem2  41684  rzalf  41689  fnchoice  41701  refsumcn  41702  rfcnnnub  41708  refsum2cnlem1  41709  iuneq2df  41723  uzwo4  41730  ixpeq2d  41745  ixpssmapc  41751  elintd  41753  ssdf  41754  ralimralim  41760  nelrnmpt  41763  ixpssixp  41771  ballss3  41772  iinssiin  41807  eliind2  41808  ralrimia  41810  rabssd  41822  fompt  41862  choicefi  41872  iunmapss  41887  iunmapsn  41889  axccdom  41896  mptfnd  41921  ssfiunibd  41984  xralrple2  42029  infxr  42042  xrralrecnnle  42060  xrralrecnnge  42069  supxrunb3  42079  fimaxre4  42081  supxrleubrnmpt  42086  rexabslelem  42098  suprleubrnmpt  42102  uzublem  42110  infxrgelbrnmpt  42136  iooiinicc  42222  iooiinioc  42236  mccl  42283  climsuse  42293  mullimc  42301  mullimcf  42308  limcrecl  42314  limsupre  42326  limcleqr  42329  addlimc  42333  0ellimcdiv  42334  limclner  42336  limsupubuzlem  42397  climinf3  42401  limsupequzmpt2  42403  limsupmnfuzlem  42411  limsupre3uzlem  42420  liminfequzmpt2  42476  cncficcgt0  42573  cncfioobd  42582  fprodsubrecnncnvlem  42592  fprodaddrecnncnvlem  42594  dvmptfprodlem  42629  dvnprodlem1  42631  iblsplitf  42655  stoweidlem5  42690  stoweidlem16  42701  stoweidlem18  42703  stoweidlem21  42706  stoweidlem26  42711  stoweidlem27  42712  stoweidlem28  42713  stoweidlem29  42714  stoweidlem31  42716  stoweidlem34  42719  stoweidlem36  42721  stoweidlem41  42726  stoweidlem42  42727  stoweidlem44  42729  stoweidlem45  42730  stoweidlem48  42733  stoweidlem51  42736  stoweidlem55  42740  stoweidlem59  42744  stoweidlem60  42745  stoweidlem62  42747  wallispilem3  42752  stirlinglem5  42763  fourierdlem16  42808  fourierdlem21  42813  fourierdlem22  42814  fourierdlem31  42823  fourierdlem39  42831  fourierdlem68  42859  fourierdlem71  42862  fourierdlem73  42864  fourierdlem77  42868  fourierdlem80  42871  fourierdlem83  42874  fourierdlem87  42878  fourierdlem94  42885  fourierdlem103  42894  fourierdlem104  42895  fourierdlem112  42903  fourierdlem113  42904  etransclem32  42951  subsaliuncllem  43040  sge0revalmpt  43060  sge0fodjrnlem  43098  sge0fsummptf  43118  iundjiun  43142  meadjiun  43148  voliunsge0lem  43154  meaiininclem  43168  omeiunle  43199  hoicvrrex  43238  ovnsubaddlem2  43253  hoissrrn2  43260  hoidmv1lelem1  43273  hoidmvlelem3  43279  ovnhoilem1  43283  hoi2toco  43289  ovnlecvr2  43292  hspdifhsp  43298  hoiqssbllem1  43304  hoiqssbllem3  43306  hspmbllem2  43309  iinhoiicclem  43355  iunhoiioolem  43357  vonioo  43364  vonicc  43367  pimconstlt0  43382  pimconstlt1  43383  pimltpnf  43384  pimiooltgt  43389  pimdecfgtioc  43393  pimincfltioc  43394  pimdecfgtioo  43395  pimincfltioo  43396  preimageiingt  43398  preimaleiinlt  43399  issmfd  43412  issmfdf  43414  sssmf  43415  issmfle  43422  issmfdmpt  43425  issmfgt  43433  issmfled  43434  issmfgtd  43437  smflimlem2  43448  smfmullem4  43469  smfpimcclem  43481  smfsuplem1  43485  smfsupmpt  43489  smfinflem  43491  smfinfmpt  43493  iccelpart  43993  mogoldbb  44346  sbgoldbo  44348  aacllem  45370
 Copyright terms: Public domain W3C validator