Theorem ralrimi 2957

Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.) Shortened after introduction of hbralrimi 2954. (Revised by Wolf Lammen, 4-Dec-2019.)

Hypotheses

Ref	Expression
ralrimi.1	|- F/ x ph
ralrimi.2	|- ( ph -> ( x e. A -> ps ) )

Assertion

Ref	Expression
ralrimi	|- ( ph -> A. x e. A ps )

Proof of Theorem ralrimi

Step	Hyp	Ref	Expression
1		ralrimi.1	. . 3 |- F/ x ph
2	1	nf5ri 2065	. 2 |- ( ph -> A. x ph )
3		ralrimi.2	. 2 |- ( ph -> ( x e. A -> ps ) )
4	2, 3	hbralrimi 2954	1 |- ( ph -> A. x e. A ps )

Syntax hints:   -> wi 4   F/wnf 1708   e. wcel 1990   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-nf 1710  df-ral 2917

This theorem is referenced by:  ralimdaa  2958  reximdai  3012  rexlimd2  3025  r19.12  3063  r19.37  3086  ralcom2  3104  2rmorex  3412  iineq2d  4541  disjxiun  4649  disjxiunOLD  4650  mpteq2da  4743  mpteqb  6299  fmptdf  6387  eusvobj2  6643  offval2f  6909  zfrep6  7134  wfrlem4  7418  tfr3  7495  tz7.49  7540  mapxpen  8126  dfac2  8953  hsmexlem4  9251  axcc3  9260  domtriomlem  9264  axdc3lem2  9273  axdc3lem4  9275  axdc4lem  9277  ac6num  9301  dedekind  10200  dedekindle  10201  fsuppmapnn0fiublem  12789  fsuppmapnn0fiub  12790  fsuppmapnn0fiubOLD  12791  fprodcllemf  14688  lcmfunsnlem1  15350  lcmfunsnlem2lem1  15351  lcmfunsnlem2  15353  mreexexd  16308  mreexexdOLD  16309  cpmatmcllem  20523  ptcnplem  21424  xkocnv  21617  cfilucfil  22364  itg2splitlem  23515  itg2split  23516  itgeq1f  23538  mptelee  25775  lfgrnloop  26020  foresf1o  29343  funimass4f  29437  fcomptf  29458  aciunf1lem  29462  funcnvmptOLD  29467  funcnvmpt  29468  isarchiofld  29817  reff  29906  locfinreflem  29907  prodindf  30085  esumeq12dvaf  30093  esumgsum  30107  esumel  30109  esumf1o  30112  esumc  30113  esummono  30116  gsumesum  30121  esumlub  30122  esumlef  30124  esumfsup  30132  esumpinfval  30135  esumpinfsum  30139  esum2d  30155  ldsysgenld  30223  sigapildsyslem  30224  ldgenpisyslem1  30226  measinblem  30283  voliune  30292  volmeas  30294  oms0  30359  omssubadd  30362  dstrvprob  30533  bnj1379  30901  bnj1204  31080  bnj1388  31101  bnj1417  31109  bnj1489  31124  untsucf  31587  trpredmintr  31731  frrlem4  31783  bj-rabbida  32914  cover2  33508  upixp  33524  indexdom  33529  filbcmb  33535  sdclem2  33538  eq0rabdioph  37340  eqrabdioph  37341  setindtr  37591  ss2iundf  37951  gneispace  38432  iunconnlem2  39171  rzalf  39176  fnchoice  39188  refsumcn  39189  rfcnnnub  39195  refsum2cnlem1  39196  iuneq2df  39212  uzwo4  39221  ixpeq2d  39237  ixpssmapc  39243  elintd  39245  ssdf  39247  ralimralim  39253  nelrnmpt  39257  ixpssixp  39269  ballss3  39270  rabbida  39274  iinssiin  39312  eliind2  39313  ralrimia  39315  rabssd  39332  fompt  39379  rnmptssd  39385  choicefi  39392  iunmapss  39407  iunmapsn  39409  rnmpt0  39412  axccdom  39416  dmmptdf  39417  axccd  39429  fnmptd  39434  dmmptdf2  39439  mptfnd  39451  mpteq12da  39452  rnmptbd2lem  39463  rnmptssdf  39469  rnmptbdlem  39470  ssfiunibd  39523  xralrple2  39570  infxr  39583  xrralrecnnle  39602  xrralrecnnge  39613  supxrunb3  39623  fimaxre4  39625  supxrleubrnmpt  39632  rexabslelem  39645  suprleubrnmpt  39649  uzublem  39657  infxrgelbrnmpt  39683  iooiinicc  39769  iooiinioc  39783  mccl  39830  climsuse  39840  mullimc  39848  mullimcf  39855  limcrecl  39861  limsupre  39873  limcleqr  39876  addlimc  39880  0ellimcdiv  39881  limclner  39883  limsupubuzlem  39944  climinf3  39948  limsupequzmpt2  39950  limsupmnfuzlem  39958  limsupre3uzlem  39967  liminfequzmpt2  40023  cncficcgt0  40101  cncfioobd  40110  cncfcompt2  40112  fprodsubrecnncnvlem  40121  fprodaddrecnncnvlem  40123  dvmptfprodlem  40159  dvnprodlem1  40161  iblsplitf  40186  stoweidlem5  40222  stoweidlem16  40233  stoweidlem18  40235  stoweidlem21  40238  stoweidlem26  40243  stoweidlem27  40244  stoweidlem28  40245  stoweidlem29  40246  stoweidlem31  40248  stoweidlem34  40251  stoweidlem36  40253  stoweidlem41  40258  stoweidlem42  40259  stoweidlem44  40261  stoweidlem45  40262  stoweidlem48  40265  stoweidlem51  40268  stoweidlem55  40272  stoweidlem59  40276  stoweidlem60  40277  stoweidlem62  40279  wallispilem3  40284  stirlinglem5  40295  fourierdlem16  40340  fourierdlem21  40345  fourierdlem22  40346  fourierdlem31  40355  fourierdlem39  40363  fourierdlem68  40391  fourierdlem71  40394  fourierdlem73  40396  fourierdlem77  40400  fourierdlem80  40403  fourierdlem83  40406  fourierdlem87  40410  fourierdlem94  40417  fourierdlem103  40426  fourierdlem104  40427  fourierdlem112  40435  fourierdlem113  40436  etransclem32  40483  subsaliuncllem  40575  sge0revalmpt  40595  sge0fodjrnlem  40633  sge0fsummptf  40653  iundjiun  40677  meadjiun  40683  voliunsge0lem  40689  meaiininclem  40700  omeiunle  40731  hoicvrrex  40770  ovnsubaddlem2  40785  hoissrrn2  40792  hoidmv1lelem1  40805  hoidmvlelem3  40811  ovnhoilem1  40815  hoi2toco  40821  ovnlecvr2  40824  hspdifhsp  40830  hoiqssbllem1  40836  hoiqssbllem3  40838  hspmbllem2  40841  iinhoiicclem  40887  iunhoiioolem  40889  vonioo  40896  vonicc  40899  pimconstlt0  40914  pimconstlt1  40915  pimltpnf  40916  pimiooltgt  40921  pimdecfgtioc  40925  pimincfltioc  40926  pimdecfgtioo  40927  pimincfltioo  40928  preimageiingt  40930  preimaleiinlt  40931  issmfd  40944  issmfdf  40946  sssmf  40947  issmfle  40954  issmfdmpt  40957  issmfgt  40965  issmfled  40966  issmfgtd  40969  smflimlem2  40980  smfmullem4  41001  smfpimcclem  41013  smfsuplem1  41017  smfsupmpt  41021  smfinflem  41023  smfinfmpt  41025  iccelpart  41369  mogoldbb  41673  sbgoldbo  41675  aacllem  42547