Theorem ralrimiv 2876

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 4-Dec-2019.)

Hypothesis

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

Assertion

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

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   A( x)

Proof of Theorem ralrimiv

Step	Hyp	Ref	Expression
1		ax-5 1680	. 2 |- ( ph -> A. x ph )
2		ralrimiv.1	. 2 |- ( ph -> ( x e. A -> ps ) )
3	1, 2	hbralrimi 2860	1 |- ( ph -> A. x e. A ps )

Syntax hints:   -> wi 4   e. wcel 1767   A.wral 2814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680

This theorem depends on definitions:  df-bi 185  df-ral 2819

This theorem is referenced by:  ralrimiva  2878  ralrimivw  2879  ralrimdv  2880  ralrimivv  2884  reximdvai  2935  r19.27av  2995  rr19.3v  3245  rabssdv  3580  rzal  3929  trin  4550  class2seteq  4615  ralxfrALT  4666  otiunsndisj  4753  onmindif  4967  issref  5380  fnprb  6119  fnprOLD  6120  ssorduni  6605  onminex  6626  onmindif2  6631  suceloni  6632  limuni3  6671  frxp  6893  poxp  6895  onfununi  7012  onnseq  7015  tfrlem12  7058  tz7.48-2  7107  oaass  7210  omass  7229  oelim2  7244  oelimcl  7249  oaabs2  7294  omabs  7296  undifixp  7505  dom2lem  7555  isinf  7733  unblem4  7775  unbnn2  7777  marypha1lem  7893  supiso  7933  ordiso2  7940  card2inf  7981  elirrv  8023  wemapwe  8139  wemapweOLD  8140  trcl  8159  tz9.13  8209  rankval3b  8244  rankunb  8268  rankuni2b  8271  scott0  8304  dfac8alem  8410  carduniima  8477  alephsmo  8483  alephval3  8491  iunfictbso  8495  dfac3  8502  dfac5lem5  8508  dfac12r  8526  dfac12k  8527  kmlem4  8533  kmlem11  8540  cfsuc  8637  cofsmo  8649  cfsmolem  8650  coftr  8653  alephsing  8656  infpssrlem3  8685  fin23lem30  8722  isf32lem2  8734  isf32lem3  8735  isf34lem6  8760  fin1a2lem11  8790  fin1a2lem13  8792  fin1a2s  8794  axcc2lem  8816  domtriomlem  8822  axdc3lem2  8831  axdc4lem  8835  axcclem  8837  axdclem2  8900  iundom2g  8915  uniimadom  8919  cardmin  8939  alephval2  8947  alephreg  8957  fpwwe2lem12  9019  wunex2  9116  wuncval2  9125  tskwe2  9151  inar1  9153  tskuni  9161  gruun  9184  intgru  9192  grutsk1  9199  genpcl  9386  ltexprlem5  9418  suplem1pr  9430  supexpr  9432  supsrlem  9488  axpre-sup  9546  supmul1  10508  supmullem1  10509  supmul  10511  peano5nni  10539  uzind  10952  zindd  10962  uzwo  11144  uzwoOLD  11145  lbzbi  11170  xrsupsslem  11498  xrinfmsslem  11499  supxrun  11507  supxrpnf  11510  supxrunb1  11511  supxrunb2  11512  icoshftf1o  11643  flval3  11919  axdc4uzlem  12060  2cshw  12744  cshweqrep  12752  sqrlem1  13039  sqrlem6  13044  fsum0diag2  13561  alzdvds  13895  gcdcllem1  14008  maxprmfct  14113  unbenlem  14285  vdwlem6  14363  vdwlem10  14367  firest  14688  mrieqv2d  14894  iscatd  14928  setcmon  15272  setcepi  15273  isglbd  15604  isacs4lem  15655  acsfiindd  15664  acsmapd  15665  psss  15701  ghmrn  16085  ghmpreima  16093  cntz2ss  16175  symgextres  16255  psgnunilem2  16326  lsmsubg  16480  efgsfo  16563  gsumzaddlem  16737  gsumzaddlemOLD  16739  gsummptnn0fzfv  16819  dmdprdd  16833  dprd2da  16893  imasrng  17069  isabvd  17269  issrngd  17310  islssd  17382  lbsextlem3  17606  lbsextlem4  17607  lidldvgen  17702  psgnghm  18411  isphld  18484  frlmsslsp  18624  frlmsslspOLD  18625  scmatscm  18810  mp2pm2mplem4  19105  tgcl  19265  distop  19291  indistopon  19296  pptbas  19303  toponmre  19388  opnnei  19415  neiuni  19417  neindisj2  19418  ordtrest2  19499  cnpnei  19559  cnindis  19587  cmpcld  19696  uncmp  19697  hauscmplem  19700  2ndc1stc  19746  1stcrest  19748  1stcelcls  19756  llyrest  19780  nllyrest  19781  cldllycmp  19790  txcls  19868  ptpjcn  19875  ptclsg  19879  dfac14lem  19881  xkoccn  19883  txlly  19900  txnlly  19901  ptrescn  19903  tx1stc  19914  xkoco1cn  19921  xkoco2cn  19922  xkococn  19924  xkoinjcn  19951  qtopeu  19980  hmeofval  20022  ordthmeolem  20065  isfild  20122  fbasrn  20148  trfil2  20151  flimclslem  20248  fclsrest  20288  fclscf  20289  flimfcls  20290  alexsubALTlem1  20310  alexsubALTlem2  20311  alexsubALTlem3  20312  alexsubALT  20314  divstgpopn  20381  isxmetd  20592  imasdsf1olem  20639  blcls  20772  prdsxmslem2  20795  metustfbasOLD  20831  metustfbas  20832  dscmet  20856  nrmmetd  20858  reperflem  21086  reconnlem2  21095  xrge0tsms  21102  fsumcn  21137  cnheibor  21218  tchcph  21443  lmmbr  21460  caubl  21509  ivthlem1  21626  ovolctb  21664  ovoliunlem2  21677  ovolscalem1  21687  ovolicc2  21696  voliunlem3  21725  ismbfd  21810  mbfimaopnlem  21825  itg2le  21909  ellimc2  22044  c1liplem1  22160  plyeq0lem  22370  dgreq0  22424  aannenlem1  22486  pilem2  22609  cxpcn3lem  22877  scvxcvx  23071  musum  23223  dchrisum0flb  23451  ostth2lem2  23575  usgrares1  24114  nbusgra  24132  nbgra0nb  24133  nbgra0edg  24136  cusgrafilem2  24184  usgrasscusgra  24187  uvtxnbgravtx  24199  fargshiftf  24340  fargshiftfva  24343  usg2wlkeq  24412  clwwlkn0  24478  clwwisshclwwlem  24510  0egra0rgra  24640  eupatrl  24672  eupap1  24680  3cyclfrgrarn  24717  vdgn1frgrav3  24733  numclwlk2lem2f1o  24810  frgraregord013  24823  htthlem  25538  ocsh  25905  shintcli  25951  pjss2coi  26787  pjnormssi  26791  pjclem4  26822  pj3si  26830  pj3cor1i  26832  strlem3a  26875  strb  26881  hstrlem3a  26883  hstrbi  26889  spansncv2  26916  mdsl1i  26944  cvmdi  26947  mdexchi  26958  h1da  26972  mdsymlem6  27031  sumdmdii  27038  dmdbr5ati  27045  isoun  27220  supssd  27227  xrge0tsmsd  27466  ordtrest2NEW  27569  pwsiga  27798  measiun  27857  dya2iocuni  27922  erdszelem8  28310  cvmsss2  28387  cvmfolem  28392  rtrclreclem.min  28573  dfrtrcl2  28574  dfon2lem8  28827  dfon2lem9  28828  dfon2  28829  rdgprc  28832  trpredtr  28918  trpredmintr  28919  trpredelss  28920  dftrpred3g  28921  trpredpo  28923  trpredrec  28926  wfrlem15  28962  frr3g  28991  frrlem5b  28997  frrlem5d  28999  sltval2  29021  supaddc  29646  supadd  29647  heicant  29654  mblfinlem1  29656  ftc2nc  29704  nn0prpwlem  29745  ntruni  29750  clsint2  29752  fneint  29777  reftr  29789  fnessref  29793  refssfne  29794  locfincf  29806  comppfsc  29807  neibastop1  29808  neibastop2lem  29809  sdclem2  29866  fdc  29869  seqpo  29871  prdsbnd  29920  heibor  29948  rrnequiv  29962  0idl  30053  intidl  30057  unichnidl  30059  prnc  30095  pellfundre  30449  pellfundge  30450  pellfundlb  30452  dford3lem1  30600  aomclem2  30633  hashgcdeq  30791  addrcom  30990  fourierdlem103  31538  funressnfv  31708  tz6.12-afv  31753  ellcoellss  32135  lindsrng01  32168  snlindsntorlem  32170  iunconlem2  32833  bnj518  33041  bnj1137  33148  bnj1136  33150  bnj1413  33188  bnj1417  33194  bnj60  33215  lsmcv2  33844  lcvexchlem4  33852  lcvexchlem5  33853  eqlkr  33914  paddclN  34656  pclfinN  34714  ldilcnv  34929  ldilco  34930  cdleme25dN  35170  cdlemj2  35636  tendocan  35638  erng1lem  35801  erngdvlem4-rN  35813  dihord2pre  36040  dihglblem2N  36109  dochvalr  36172  hdmap14lem12  36697  hdmap14lem13  36698