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

Theorem ralrimi 3216
Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.) Shortened after introduction of hbralrimi 3180. (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 2185 . 2 (𝜑 → ∀𝑥𝜑)
3 ralrimi.2 . 2 (𝜑 → (𝑥𝐴𝜓))
42, 3hbralrimi 3180 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1775  wcel 2105  wral 3138
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-ex 1772  df-nf 1776  df-ral 3143
This theorem is referenced by:  ralimdaa  3217  reximdai  3311  rexlimd2  3316  r19.12  3324  r19.12OLD  3327  r19.37  3343  ralcom2w  3363  ralcom2  3364  rabbida  3475  2rmorex  3744  iineq2d  4934  disjxiun  5055  mpteq2da  5152  fnmptd  6483  mpteqb  6780  fmptdf  6874  eusvobj2  7138  offval2f  7410  zfrep6  7647  wfrlem4  7949  tfr3  8026  tz7.49  8072  mapxpen  8672  dfac2b  9545  hsmexlem4  9840  axcc3  9849  domtriomlem  9853  axdc3lem2  9862  axdc3lem4  9864  axdc4lem  9866  ac6num  9890  dedekind  10792  dedekindle  10793  fsuppmapnn0fiublem  13348  fsuppmapnn0fiub  13349  fprodcllemf  15302  lcmfunsnlem1  15971  lcmfunsnlem2lem1  15972  lcmfunsnlem2  15974  mreexexd  16909  cpmatmcllem  21256  ptcnplem  22159  xkocnv  22352  cfilucfil  23098  itg2splitlem  24278  itg2split  24279  itgeq1f  24301  mptelee  26609  lfgrnloop  26838  foresf1o  30193  funimass4f  30311  fcomptf  30332  aciunf1lem  30336  funcnvmpt  30341  fnpreimac  30345  isarchiofld  30818  reff  31003  locfinreflem  31004  prodindf  31182  esumeq12dvaf  31190  esumgsum  31204  esumel  31206  esumf1o  31209  esumc  31210  esummono  31213  gsumesum  31218  esumlub  31219  esumlef  31221  esumfsup  31229  esumpinfval  31232  esumpinfsum  31236  esum2d  31252  ldsysgenld  31319  sigapildsyslem  31320  ldgenpisyslem1  31322  measinblem  31379  voliune  31388  volmeas  31390  oms0  31455  omssubadd  31458  dstrvprob  31629  bnj1379  32002  bnj1204  32182  bnj1388  32203  bnj1417  32211  bnj1489  32226  untsucf  32834  trpredmintr  32968  frrlem4  33024  domalom  34568  fvineqsneq  34576  cover2  34872  upixp  34887  indexdom  34892  filbcmb  34898  sdclem2  34900  eq0rabdioph  39253  eqrabdioph  39254  setindtr  39501  ss2iundf  39884  gneispace  40364  mnuprdlem3  40490  iunconnlem2  41149  rzalf  41154  fnchoice  41166  refsumcn  41167  rfcnnnub  41173  refsum2cnlem1  41174  iuneq2df  41188  uzwo4  41195  ixpeq2d  41210  ixpssmapc  41216  elintd  41218  ssdf  41219  ralimralim  41225  nelrnmpt  41228  ixpssixp  41238  ballss3  41239  iinssiin  41275  eliind2  41276  ralrimia  41278  rabssd  41291  fompt  41333  choicefi  41343  iunmapss  41358  iunmapsn  41360  axccdom  41367  mptfnd  41392  ssfiunibd  41456  xralrple2  41502  infxr  41515  xrralrecnnle  41533  xrralrecnnge  41542  supxrunb3  41552  fimaxre4  41554  supxrleubrnmpt  41559  rexabslelem  41572  suprleubrnmpt  41576  uzublem  41584  infxrgelbrnmpt  41610  iooiinicc  41698  iooiinioc  41712  mccl  41759  climsuse  41769  mullimc  41777  mullimcf  41784  limcrecl  41790  limsupre  41802  limcleqr  41805  addlimc  41809  0ellimcdiv  41810  limclner  41812  limsupubuzlem  41873  climinf3  41877  limsupequzmpt2  41879  limsupmnfuzlem  41887  limsupre3uzlem  41896  liminfequzmpt2  41952  cncficcgt0  42051  cncfioobd  42060  cncfcompt2  42062  fprodsubrecnncnvlem  42071  fprodaddrecnncnvlem  42073  dvmptfprodlem  42109  dvnprodlem1  42111  iblsplitf  42135  stoweidlem5  42171  stoweidlem16  42182  stoweidlem18  42184  stoweidlem21  42187  stoweidlem26  42192  stoweidlem27  42193  stoweidlem28  42194  stoweidlem29  42195  stoweidlem31  42197  stoweidlem34  42200  stoweidlem36  42202  stoweidlem41  42207  stoweidlem42  42208  stoweidlem44  42210  stoweidlem45  42211  stoweidlem48  42214  stoweidlem51  42217  stoweidlem55  42221  stoweidlem59  42225  stoweidlem60  42226  stoweidlem62  42228  wallispilem3  42233  stirlinglem5  42244  fourierdlem16  42289  fourierdlem21  42294  fourierdlem22  42295  fourierdlem31  42304  fourierdlem39  42312  fourierdlem68  42340  fourierdlem71  42343  fourierdlem73  42345  fourierdlem77  42349  fourierdlem80  42352  fourierdlem83  42355  fourierdlem87  42359  fourierdlem94  42366  fourierdlem103  42375  fourierdlem104  42376  fourierdlem112  42384  fourierdlem113  42385  etransclem32  42432  subsaliuncllem  42521  sge0revalmpt  42541  sge0fodjrnlem  42579  sge0fsummptf  42599  iundjiun  42623  meadjiun  42629  voliunsge0lem  42635  meaiininclem  42649  omeiunle  42680  hoicvrrex  42719  ovnsubaddlem2  42734  hoissrrn2  42741  hoidmv1lelem1  42754  hoidmvlelem3  42760  ovnhoilem1  42764  hoi2toco  42770  ovnlecvr2  42773  hspdifhsp  42779  hoiqssbllem1  42785  hoiqssbllem3  42787  hspmbllem2  42790  iinhoiicclem  42836  iunhoiioolem  42838  vonioo  42845  vonicc  42848  pimconstlt0  42863  pimconstlt1  42864  pimltpnf  42865  pimiooltgt  42870  pimdecfgtioc  42874  pimincfltioc  42875  pimdecfgtioo  42876  pimincfltioo  42877  preimageiingt  42879  preimaleiinlt  42880  issmfd  42893  issmfdf  42895  sssmf  42896  issmfle  42903  issmfdmpt  42906  issmfgt  42914  issmfled  42915  issmfgtd  42918  smflimlem2  42929  smfmullem4  42950  smfpimcclem  42962  smfsuplem1  42966  smfsupmpt  42970  smfinflem  42972  smfinfmpt  42974  iccelpart  43440  mogoldbb  43797  sbgoldbo  43799  aacllem  44800
  Copyright terms: Public domain W3C validator