Theorem ralrimiv 2808

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 1766	. 2 |- ( ph -> A. x ph )
2		ralrimiv.1	. 2 |- ( ph -> ( x e. A -> ps ) )
3	1, 2	hbralrimi 2797	1 |- ( ph -> A. x e. A ps )

Syntax hints:   -> wi 4   e. wcel 1904   A.wral 2756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766

This theorem depends on definitions:  df-bi 190  df-ral 2761

This theorem is referenced by:  ralrimiva  2809  ralrimivw  2810  ralrimdv  2811  ralrimivv  2813  reximdvai  2856  r19.27v  2910  raleleq  2991  rr19.3v  3168  rabssdv  3495  rzal  3862  trin  4500  class2seteq  4569  ralxfrALT  4619  otiunsndisj  4707  issref  5219  onmindif  5519  fnprb  6139  fntpb  6140  ssorduni  6631  onminex  6653  onmindif2  6658  suceloni  6659  limuni3  6698  frxp  6925  poxp  6927  wfrlem15  7068  onfununi  7078  onnseq  7081  tfrlem12  7125  tz7.48-2  7177  oaass  7280  omass  7299  oelim2  7314  oelimcl  7319  oaabs2  7364  omabs  7366  undifixp  7576  dom2lem  7627  isinf  7803  unblem4  7844  unbnn2  7846  marypha1lem  7965  supiso  8009  ordiso2  8048  card2inf  8088  elirrv  8130  wemapwe  8220  trcl  8230  tz9.13  8280  rankval3b  8315  rankunb  8339  rankuni2b  8342  scott0  8375  dfac8alem  8478  carduniima  8545  alephsmo  8551  alephval3  8559  iunfictbso  8563  dfac3  8570  dfac5lem5  8576  dfac12r  8594  dfac12k  8595  kmlem4  8601  kmlem11  8608  cfsuc  8705  cofsmo  8717  cfsmolem  8718  coftr  8721  alephsing  8724  infpssrlem3  8753  fin23lem30  8790  isf32lem2  8802  isf32lem3  8803  isf34lem6  8828  fin1a2lem11  8858  fin1a2lem13  8860  fin1a2s  8862  axcc2lem  8884  domtriomlem  8890  axdc3lem2  8899  axdc4lem  8903  axcclem  8905  axdclem2  8968  iundom2g  8983  uniimadom  8987  cardmin  9007  alephval2  9015  alephreg  9025  fpwwe2lem12  9084  wunex2  9181  wuncval2  9190  tskwe2  9216  inar1  9218  tskuni  9226  gruun  9249  intgru  9257  grutsk1  9264  genpcl  9451  ltexprlem5  9483  suplem1pr  9495  supexpr  9497  supsrlem  9553  axpre-sup  9611  fiminre  10577  supaddc  10596  supadd  10597  supmul1  10598  supmullem1  10599  supmul  10601  peano5nni  10634  uzind  11050  zindd  11059  uzwo  11245  lbzbi  11275  xrsupsslem  11617  xrinfmsslem  11618  supxrun  11626  supxrpnf  11629  supxrunb1  11630  supxrunb2  11631  icoshftf1o  11781  flval3  12083  axdc4uzlem  12233  ccatrn  12784  2cshw  12969  cshweqrep  12977  rtrclreclem4  13201  dfrtrcl2  13202  sqrlem1  13383  sqrlem6  13388  fsum0diag2  13921  alzdvds  14432  gcdcllem1  14552  lcmfunsnlem2lem1  14690  lcmfunsnlem2lem2  14691  maxprmfct  14731  unbenlem  14931  vdwlem6  15015  vdwlem10  15019  firest  15409  mrieqv2d  15623  iscatd  15657  setcmon  16060  setcepi  16061  fullestrcsetc  16114  fullsetcestrc  16129  isglbd  16441  isacs4lem  16492  acsfiindd  16501  acsmapd  16502  psss  16538  ghmrn  16974  ghmpreima  16982  cntz2ss  17064  symgextres  17144  psgnunilem2  17214  lsmsubg  17384  efgsfo  17467  gsumzaddlem  17632  gsummptnn0fzfv  17695  dmdprdd  17709  dprd2da  17753  imasring  17925  isabvd  18126  issrngd  18167  islssd  18237  lbsextlem3  18461  lbsextlem4  18462  lidldvgen  18556  psgnghm  19225  isphld  19298  frlmsslsp  19431  mp2pm2mplem4  19910  tgcl  20062  distop  20088  indistopon  20093  pptbas  20100  toponmre  20186  opnnei  20213  neiuni  20215  neindisj2  20216  ordtrest2  20297  cnpnei  20357  cnindis  20385  cmpcld  20494  uncmp  20495  hauscmplem  20498  2ndc1stc  20543  1stcrest  20545  1stcelcls  20553  llyrest  20577  nllyrest  20578  cldllycmp  20587  reftr  20606  locfincf  20623  comppfsc  20624  txcls  20696  ptpjcn  20703  ptclsg  20707  dfac14lem  20709  xkoccn  20711  txlly  20728  txnlly  20729  ptrescn  20731  tx1stc  20742  xkoco1cn  20749  xkoco2cn  20750  xkococn  20752  xkoinjcn  20779  qtopeu  20808  hmeofval  20850  ordthmeolem  20893  isfild  20951  fbasrn  20977  trfil2  20980  flimclslem  21077  fclsrest  21117  fclscf  21118  flimfcls  21119  alexsubALTlem1  21140  alexsubALTlem2  21141  alexsubALTlem3  21142  alexsubALT  21144  qustgpopn  21212  isxmetd  21419  imasdsf1olem  21466  blcls  21599  prdsxmslem2  21622  metustfbas  21650  dscmet  21665  nrmmetd  21667  reperflem  21914  reconnlem2  21923  xrge0tsms  21930  fsumcn  21980  cnheibor  22061  tchcph  22289  lmmbr  22306  caubl  22355  ivthlem1  22480  ovolctb  22521  ovoliunlem2  22534  ovolscalem1  22544  ovolicc2  22554  voliunlem3  22584  ismbfd  22675  mbfimaopnlem  22690  itg2le  22776  ellimc2  22911  c1liplem1  23027  plyeq0lem  23243  dgreq0  23298  aannenlem1  23363  pilem2  23486  pilem2OLD  23487  cxpcn3lem  23766  scvxcvx  23990  musum  24199  dchrisum0flb  24427  ostth2lem2  24551  usgrares1  25217  nbusgra  25235  nbgra0nb  25236  nbgra0edg  25239  cusgrafilem2  25287  usgrasscusgra  25290  uvtxnbgravtx  25302  fargshiftf  25443  fargshiftfva  25446  usg2wlkeq  25515  clwwlkn0  25581  clwwisshclwwlem  25613  0egra0rgra  25743  eupatrl  25775  eupap1  25783  3cyclfrgrarn  25820  vdgn1frgrav3  25835  2spotiundisj  25869  numclwlk2lem2f1o  25912  frgraregord013  25925  htthlem  26651  ocsh  27017  shintcli  27063  pjss2coi  27898  pjnormssi  27902  pjclem4  27933  pj3si  27941  pj3cor1i  27943  strlem3a  27986  strb  27992  hstrlem3a  27994  hstrbi  28000  spansncv2  28027  mdsl1i  28055  cvmdi  28058  mdexchi  28069  h1da  28083  mdsymlem6  28142  sumdmdii  28149  dmdbr5ati  28156  isoun  28357  supssd  28365  infssd  28366  xrge0tsmsd  28622  ordtrest2NEW  28803  pwsiga  29026  measiun  29114  dya2iocuni  29178  bnj518  29769  bnj1137  29876  bnj1136  29878  bnj1413  29916  bnj1417  29922  bnj60  29943  erdszelem8  29993  cvmsss2  30069  cvmfolem  30074  dfon2lem8  30507  dfon2lem9  30508  dfon2  30509  rdgprc  30512  trpredtr  30542  trpredmintr  30543  trpredelss  30544  dftrpred3g  30545  trpredpo  30547  trpredrec  30550  frr3g  30584  frrlem5b  30590  frrlem5d  30592  sltval2  30614  nn0prpwlem  31049  ntruni  31054  clsint2  31056  fneint  31075  fnessref  31084  refssfne  31085  neibastop1  31086  neibastop2lem  31087  relowlpssretop  31837  heicant  32039  mblfinlem1  32041  ftc2nc  32090  sdclem2  32135  fdc  32138  seqpo  32140  prdsbnd  32189  heibor  32217  rrnequiv  32231  0idl  32322  intidl  32326  unichnidl  32328  prnc  32364  lsmcv2  32666  lcvexchlem4  32674  lcvexchlem5  32675  eqlkr  32736  paddclN  33478  pclfinN  33536  ldilcnv  33751  ldilco  33752  cdleme25dN  33994  cdlemj2  34460  tendocan  34462  erng1lem  34625  erngdvlem4-rN  34637  dihord2pre  34864  dihglblem2N  34933  dochvalr  34996  hdmap14lem12  35521  hdmap14lem13  35522  pellfundre  35800  pellfundge  35801  pellfundlb  35803  dford3lem1  35952  aomclem2  35984  hashgcdeq  36146  pwinfi3  36238  iunrelexp0  36365  iunrelexpmin1  36371  iunrelexpmin2  36375  dftrcl3  36383  cnvtrclfv  36387  trclimalb2  36389  dfrtrcl3  36396  addrcom  36898  iunconlem2  37395  ssuzfz  37659  dvmptfprod  37917  dvnprodlem3  37920  funressnfv  38774  tz6.12-afv  38820  iccpartltu  38884  iccpartgtl  38885  iccpartleu  38887  iccpartgel  38888  bgoldbst  39024  bgoldbtbnd  39049  tgblthelfgott  39053  otiunsndisjX  39152  nbuhgr  39575  nbumgr  39579  uhgrnbgr0nb  39586  uvtxanbgrvtx  39629  cusgrfilem2  39682  nnsgrp  40325  ellcoellss  40736  lindsrng01  40769  suppdm  40812  nn0sumshdiglem1  40940