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

Theorem ralrimi 2940
 Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.) Shortened after introduction of hbralrimi 2937. (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 2053 . 2 (𝜑 → ∀𝑥𝜑)
3 ralrimi.2 . 2 (𝜑 → (𝑥𝐴𝜓))
42, 3hbralrimi 2937 1 (𝜑 → ∀𝑥𝐴 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  Ⅎwnf 1699   ∈ wcel 1977  ∀wral 2896 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034 This theorem depends on definitions:  df-bi 196  df-ex 1696  df-nf 1701  df-ral 2901 This theorem is referenced by:  ralimdaa  2941  reximdai  2995  rexlimd2  3007  r19.12  3045  r19.37  3067  ralcom2  3083  2rmorex  3379  iineq2d  4477  disjxiun  4579  disjxiunOLD  4580  mpteq2da  4671  mpteqb  6207  fmptdf  6294  eusvobj2  6542  offval2f  6807  zfrep6  7027  wfrlem4  7305  tfr3  7382  tz7.49  7427  mapxpen  8011  dfac2  8836  hsmexlem4  9134  axcc3  9143  domtriomlem  9147  axdc3lem2  9156  axdc3lem4  9158  axdc4lem  9160  ac6num  9184  dedekind  10079  dedekindle  10080  fsuppmapnn0fiublem  12651  fsuppmapnn0fiub  12652  fsuppmapnn0fiubOLD  12653  fprodcllemf  14527  lcmfunsnlem1  15188  lcmfunsnlem2lem1  15189  lcmfunsnlem2  15191  mreexexd  16131  mreexexdOLD  16132  cpmatmcllem  20342  ptcnplem  21234  xkocnv  21427  cfilucfil  22174  itg2splitlem  23321  itg2split  23322  itgeq1f  23344  mptelee  25575  lfgrnloop  25791  foresf1o  28727  funimass4f  28818  fcomptf  28840  aciunf1lem  28844  funcnvmptOLD  28850  funcnvmpt  28851  isarchiofld  29148  reff  29234  locfinreflem  29235  esumeq12dvaf  29420  esumgsum  29434  esumel  29436  esumf1o  29439  esumc  29440  esummono  29443  gsumesum  29448  esumlub  29449  esumlef  29451  esumfsup  29459  esumpinfval  29462  esumpinfsum  29466  esum2d  29482  ldsysgenld  29550  sigapildsyslem  29551  ldgenpisyslem1  29553  measinblem  29610  voliune  29619  volmeas  29621  oms0  29686  omssubadd  29689  dstrvprob  29860  bnj1379  30155  bnj1204  30334  bnj1388  30355  bnj1417  30363  bnj1489  30378  untsucf  30841  trpredmintr  30975  frrlem4  31027  bj-rabbida  32106  cover2  32678  upixp  32694  indexdom  32699  filbcmb  32705  sdclem2  32708  eq0rabdioph  36358  eqrabdioph  36359  setindtr  36609  ss2iundf  36970  gneispace  37452  iunconlem2  38193  rzalf  38199  fnchoice  38211  refsumcn  38212  rfcnnnub  38218  refsum2cnlem1  38219  iuneq2df  38237  uzwo4  38246  ixpeq2d  38262  ixpssmapc  38269  elintd  38271  ssdf  38273  ralimralim  38279  nelrnmpt  38283  ixpssixp  38297  ballss3  38298  rabbida  38302  fompt  38374  rnmptssd  38380  choicefi  38387  iunmapss  38402  iunmapsn  38404  rnmpt0  38407  axccdom  38411  dmmptdf  38412  axccd  38424  ssfiunibd  38464  xralrple2  38511  infxr  38524  xrralrecnnle  38543  xrralrecnnge  38554  iooiinicc  38616  iooiinioc  38630  mccl  38665  climsuse  38675  mullimc  38683  mullimcf  38690  limcrecl  38696  limsupre  38708  limcleqr  38711  addlimc  38715  0ellimcdiv  38716  limclner  38718  cncficcgt0  38774  cncfioobd  38783  cncfcompt2  38785  fprodsubrecnncnvlem  38794  fprodaddrecnncnvlem  38796  dvmptfprodlem  38834  dvnprodlem1  38836  iblsplitf  38862  stoweidlem5  38898  stoweidlem16  38909  stoweidlem18  38911  stoweidlem21  38914  stoweidlem26  38919  stoweidlem27  38920  stoweidlem28  38921  stoweidlem29  38922  stoweidlem31  38924  stoweidlem34  38927  stoweidlem36  38929  stoweidlem41  38934  stoweidlem42  38935  stoweidlem44  38937  stoweidlem45  38938  stoweidlem48  38941  stoweidlem51  38944  stoweidlem55  38948  stoweidlem59  38952  stoweidlem60  38953  stoweidlem62  38955  wallispilem3  38960  stirlinglem5  38971  fourierdlem16  39016  fourierdlem21  39021  fourierdlem22  39022  fourierdlem31  39031  fourierdlem39  39039  fourierdlem68  39067  fourierdlem71  39070  fourierdlem73  39072  fourierdlem77  39076  fourierdlem80  39079  fourierdlem83  39082  fourierdlem87  39086  fourierdlem94  39093  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  fourierdlem113  39112  etransclem32  39159  subsaliuncllem  39251  sge0revalmpt  39271  sge0fodjrnlem  39309  sge0fsummptf  39329  iundjiun  39353  meadjiun  39359  voliunsge0lem  39365  meaiininclem  39376  omeiunle  39407  hoicvrrex  39446  ovnsubaddlem2  39461  hoissrrn2  39468  hoidmv1lelem1  39481  hoidmvlelem3  39487  ovnhoilem1  39491  hoi2toco  39497  ovnlecvr2  39500  hspdifhsp  39506  hoiqssbllem1  39512  hoiqssbllem3  39514  hspmbllem2  39517  iinhoiicclem  39564  iunhoiioolem  39566  vonioo  39573  vonicc  39576  pimconstlt0  39591  pimconstlt1  39592  pimltpnf  39593  pimiooltgt  39598  pimdecfgtioc  39602  pimincfltioc  39603  pimdecfgtioo  39604  pimincfltioo  39605  preimageiingt  39607  preimaleiinlt  39608  issmfd  39621  issmfdf  39624  sssmf  39625  issmfle  39632  issmfdmpt  39635  issmfgt  39643  issmfled  39644  issmfgtd  39647  smflimlem2  39658  smfmullem4  39679  iccelpart  39971  aacllem  42356
 Copyright terms: Public domain W3C validator