MPE Home 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  4472  disjxiun  4574  disjxiunOLD  4575  mpteq2da  4666  mpteqb  6192  fmptdf  6279  eusvobj2  6520  offval2f  6785  zfrep6  7005  wfrlem4  7283  tfr3  7360  tz7.49  7405  mapxpen  7989  dfac2  8814  hsmexlem4  9112  axcc3  9121  domtriomlem  9125  axdc3lem2  9134  axdc3lem4  9136  axdc4lem  9138  ac6num  9162  dedekind  10052  dedekindle  10053  fsuppmapnn0fiublem  12609  fsuppmapnn0fiub  12610  fsuppmapnn0fiubOLD  12611  fprodcllemf  14476  lcmfunsnlem1  15137  lcmfunsnlem2lem1  15138  lcmfunsnlem2  15140  mreexexd  16080  mreexexdOLD  16081  cpmatmcllem  20290  ptcnplem  21182  xkocnv  21375  cfilucfil  22122  itg2splitlem  23266  itg2split  23267  itgeq1f  23289  mptelee  25521  foresf1o  28521  funimass4f  28612  fcomptf  28634  aciunf1lem  28638  funcnvmptOLD  28644  funcnvmpt  28645  isarchiofld  28942  reff  29028  locfinreflem  29029  esumeq12dvaf  29214  esumgsum  29228  esumel  29230  esumf1o  29233  esumc  29234  esummono  29237  gsumesum  29242  esumlub  29243  esumlef  29245  esumfsup  29253  esumpinfval  29256  esumpinfsum  29260  esum2d  29276  ldsysgenld  29344  sigapildsyslem  29345  ldgenpisyslem1  29347  measinblem  29404  voliune  29413  volmeas  29415  oms0  29480  omssubadd  29483  dstrvprob  29654  bnj1379  29949  bnj1204  30128  bnj1388  30149  bnj1417  30157  bnj1489  30172  untsucf  30635  trpredmintr  30769  frrlem4  30821  bj-rabbida  31900  cover2  32472  upixp  32488  indexdom  32493  filbcmb  32499  sdclem2  32502  eq0rabdioph  36152  eqrabdioph  36153  setindtr  36403  ss2iundf  36764  gneispace  37246  iunconlem2  37987  rzalf  37993  fnchoice  38005  refsumcn  38006  rfcnnnub  38012  refsum2cnlem1  38013  iuneq2df  38031  uzwo4  38040  ixpeq2d  38056  ixpssmapc  38063  elintd  38065  ssdf  38067  ralimralim  38073  nelrnmpt  38077  ixpssixp  38091  ballss3  38092  rabbida  38096  fompt  38168  rnmptssd  38174  choicefi  38181  iunmapss  38196  iunmapsn  38198  rnmpt0  38201  axccdom  38205  dmmptdf  38206  axccd  38218  ssfiunibd  38258  xralrple2  38305  infxr  38318  xrralrecnnle  38337  xrralrecnnge  38348  iooiinicc  38410  iooiinioc  38424  mccl  38459  climsuse  38469  mullimc  38477  mullimcf  38484  limcrecl  38490  limsupre  38502  limcleqr  38505  addlimc  38509  0ellimcdiv  38510  limclner  38512  cncficcgt0  38568  cncfioobd  38577  cncfcompt2  38579  fprodsubrecnncnvlem  38588  fprodaddrecnncnvlem  38590  dvmptfprodlem  38628  dvnprodlem1  38630  iblsplitf  38656  stoweidlem5  38692  stoweidlem16  38703  stoweidlem18  38705  stoweidlem21  38708  stoweidlem26  38713  stoweidlem27  38714  stoweidlem28  38715  stoweidlem29  38716  stoweidlem31  38718  stoweidlem34  38721  stoweidlem36  38723  stoweidlem41  38728  stoweidlem42  38729  stoweidlem44  38731  stoweidlem45  38732  stoweidlem48  38735  stoweidlem51  38738  stoweidlem55  38742  stoweidlem59  38746  stoweidlem60  38747  stoweidlem62  38749  wallispilem3  38754  stirlinglem5  38765  fourierdlem16  38810  fourierdlem21  38815  fourierdlem22  38816  fourierdlem31  38825  fourierdlem39  38833  fourierdlem68  38861  fourierdlem71  38864  fourierdlem73  38866  fourierdlem77  38870  fourierdlem80  38873  fourierdlem83  38876  fourierdlem87  38880  fourierdlem94  38887  fourierdlem103  38896  fourierdlem104  38897  fourierdlem112  38905  fourierdlem113  38906  etransclem32  38953  subsaliuncllem  39045  sge0revalmpt  39065  sge0fodjrnlem  39103  sge0fsummptf  39123  iundjiun  39147  meadjiun  39153  voliunsge0lem  39159  meaiininclem  39170  omeiunle  39201  hoicvrrex  39240  ovnsubaddlem2  39255  hoissrrn2  39262  hoidmv1lelem1  39275  hoidmvlelem3  39281  ovnhoilem1  39285  hoi2toco  39291  ovnlecvr2  39294  hspdifhsp  39300  hoiqssbllem1  39306  hoiqssbllem3  39308  hspmbllem2  39311  iinhoiicclem  39358  iunhoiioolem  39360  vonioo  39367  vonicc  39370  pimconstlt0  39385  pimconstlt1  39386  pimltpnf  39387  pimiooltgt  39392  pimdecfgtioc  39396  pimincfltioc  39397  pimdecfgtioo  39398  pimincfltioo  39399  preimageiingt  39401  preimaleiinlt  39402  issmfd  39415  issmfdf  39418  sssmf  39419  issmfle  39426  issmfdmpt  39429  issmfgt  39437  issmfled  39438  issmfgtd  39441  smflimlem2  39452  smfmullem4  39473  iccelpart  39766  lfgrnloop  40342  aacllem  42309
  Copyright terms: Public domain W3C validator