Theorem ralrimiv 2799

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

Syntax hints:   -> wi 4   e. wcel 1886   A.wral 2736

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757

This theorem depends on definitions:  df-bi 189  df-ral 2741

This theorem is referenced by:  ralrimiva  2801  ralrimivw  2802  ralrimdv  2803  ralrimivv  2807  reximdvai  2858  r19.27v  2922  raleleq  3004  rr19.3v  3179  rabssdv  3508  rzal  3870  trin  4506  class2seteq  4570  ralxfrALT  4618  otiunsndisj  4706  issref  5212  onmindif  5511  fnprb  6121  ssorduni  6609  onminex  6631  onmindif2  6636  suceloni  6637  limuni3  6676  frxp  6903  poxp  6905  wfrlem15  7047  onfununi  7057  onnseq  7060  tfrlem12  7104  tz7.48-2  7156  oaass  7259  omass  7278  oelim2  7293  oelimcl  7298  oaabs2  7343  omabs  7345  undifixp  7555  dom2lem  7606  isinf  7782  unblem4  7823  unbnn2  7825  marypha1lem  7944  supiso  7988  ordiso2  8027  card2inf  8067  elirrv  8109  wemapwe  8199  trcl  8209  tz9.13  8259  rankval3b  8294  rankunb  8318  rankuni2b  8321  scott0  8354  dfac8alem  8457  carduniima  8524  alephsmo  8530  alephval3  8538  iunfictbso  8542  dfac3  8549  dfac5lem5  8555  dfac12r  8573  dfac12k  8574  kmlem4  8580  kmlem11  8587  cfsuc  8684  cofsmo  8696  cfsmolem  8697  coftr  8700  alephsing  8703  infpssrlem3  8732  fin23lem30  8769  isf32lem2  8781  isf32lem3  8782  isf34lem6  8807  fin1a2lem11  8837  fin1a2lem13  8839  fin1a2s  8841  axcc2lem  8863  domtriomlem  8869  axdc3lem2  8878  axdc4lem  8882  axcclem  8884  axdclem2  8947  iundom2g  8962  uniimadom  8966  cardmin  8986  alephval2  8994  alephreg  9004  fpwwe2lem12  9063  wunex2  9160  wuncval2  9169  tskwe2  9195  inar1  9197  tskuni  9205  gruun  9228  intgru  9236  grutsk1  9243  genpcl  9430  ltexprlem5  9462  suplem1pr  9474  supexpr  9476  supsrlem  9532  axpre-sup  9590  fiminre  10552  supaddc  10571  supadd  10572  supmul1  10573  supmullem1  10574  supmul  10576  peano5nni  10609  uzind  11024  zindd  11033  uzwo  11219  lbzbi  11249  xrsupsslem  11589  xrinfmsslem  11590  supxrun  11598  supxrpnf  11601  supxrunb1  11602  supxrunb2  11603  icoshftf1o  11752  flval3  12047  axdc4uzlem  12192  ccatrn  12730  2cshw  12907  cshweqrep  12915  rtrclreclem4  13117  dfrtrcl2  13118  sqrlem1  13299  sqrlem6  13304  fsum0diag2  13837  alzdvds  14348  gcdcllem1  14466  lcmfunsnlem2lem1  14604  lcmfunsnlem2lem2  14605  maxprmfct  14645  unbenlem  14845  vdwlem6  14929  vdwlem10  14933  firest  15324  mrieqv2d  15538  iscatd  15572  setcmon  15975  setcepi  15976  fullestrcsetc  16029  fullsetcestrc  16044  isglbd  16356  isacs4lem  16407  acsfiindd  16416  acsmapd  16417  psss  16453  ghmrn  16889  ghmpreima  16897  cntz2ss  16979  symgextres  17059  psgnunilem2  17129  lsmsubg  17299  efgsfo  17382  gsumzaddlem  17547  gsummptnn0fzfv  17610  dmdprdd  17624  dprd2da  17668  imasring  17840  isabvd  18041  issrngd  18082  islssd  18152  lbsextlem3  18376  lbsextlem4  18377  lidldvgen  18472  psgnghm  19141  isphld  19214  frlmsslsp  19347  mp2pm2mplem4  19826  tgcl  19978  distop  20004  indistopon  20009  pptbas  20016  toponmre  20102  opnnei  20129  neiuni  20131  neindisj2  20132  ordtrest2  20213  cnpnei  20273  cnindis  20301  cmpcld  20410  uncmp  20411  hauscmplem  20414  2ndc1stc  20459  1stcrest  20461  1stcelcls  20469  llyrest  20493  nllyrest  20494  cldllycmp  20503  reftr  20522  locfincf  20539  comppfsc  20540  txcls  20612  ptpjcn  20619  ptclsg  20623  dfac14lem  20625  xkoccn  20627  txlly  20644  txnlly  20645  ptrescn  20647  tx1stc  20658  xkoco1cn  20665  xkoco2cn  20666  xkococn  20668  xkoinjcn  20695  qtopeu  20724  hmeofval  20766  ordthmeolem  20809  isfild  20866  fbasrn  20892  trfil2  20895  flimclslem  20992  fclsrest  21032  fclscf  21033  flimfcls  21034  alexsubALTlem1  21055  alexsubALTlem2  21056  alexsubALTlem3  21057  alexsubALT  21059  qustgpopn  21127  isxmetd  21334  imasdsf1olem  21381  blcls  21514  prdsxmslem2  21537  metustfbas  21565  dscmet  21580  nrmmetd  21582  reperflem  21829  reconnlem2  21838  xrge0tsms  21845  fsumcn  21895  cnheibor  21976  tchcph  22204  lmmbr  22221  caubl  22270  ivthlem1  22395  ovolctb  22436  ovoliunlem2  22449  ovolscalem1  22459  ovolicc2  22469  voliunlem3  22498  ismbfd  22589  mbfimaopnlem  22604  itg2le  22690  ellimc2  22825  c1liplem1  22941  plyeq0lem  23157  dgreq0  23212  aannenlem1  23277  pilem2  23400  pilem2OLD  23401  cxpcn3lem  23680  scvxcvx  23904  musum  24113  dchrisum0flb  24341  ostth2lem2  24465  usgrares1  25131  nbusgra  25149  nbgra0nb  25150  nbgra0edg  25153  cusgrafilem2  25201  usgrasscusgra  25204  uvtxnbgravtx  25216  fargshiftf  25357  fargshiftfva  25360  usg2wlkeq  25429  clwwlkn0  25495  clwwisshclwwlem  25527  0egra0rgra  25657  eupatrl  25689  eupap1  25697  3cyclfrgrarn  25734  vdgn1frgrav3  25749  2spotiundisj  25783  numclwlk2lem2f1o  25826  frgraregord013  25839  htthlem  26563  ocsh  26929  shintcli  26975  pjss2coi  27810  pjnormssi  27814  pjclem4  27845  pj3si  27853  pj3cor1i  27855  strlem3a  27898  strb  27904  hstrlem3a  27906  hstrbi  27912  spansncv2  27939  mdsl1i  27967  cvmdi  27970  mdexchi  27981  h1da  27995  mdsymlem6  28054  sumdmdii  28061  dmdbr5ati  28068  isoun  28275  supssd  28283  infssd  28284  xrge0tsmsd  28541  ordtrest2NEW  28722  pwsiga  28945  measiun  29033  dya2iocuni  29098  bnj518  29690  bnj1137  29797  bnj1136  29799  bnj1413  29837  bnj1417  29843  bnj60  29864  erdszelem8  29914  cvmsss2  29990  cvmfolem  29995  dfon2lem8  30429  dfon2lem9  30430  dfon2  30431  rdgprc  30434  trpredtr  30464  trpredmintr  30465  trpredelss  30466  dftrpred3g  30467  trpredpo  30469  trpredrec  30472  frr3g  30506  frrlem5b  30512  frrlem5d  30514  sltval2  30536  nn0prpwlem  30971  ntruni  30976  clsint2  30978  fneint  30997  fnessref  31006  refssfne  31007  neibastop1  31008  neibastop2lem  31009  relowlpssretop  31760  heicant  31968  mblfinlem1  31970  ftc2nc  32019  sdclem2  32064  fdc  32067  seqpo  32069  prdsbnd  32118  heibor  32146  rrnequiv  32160  0idl  32251  intidl  32255  unichnidl  32257  prnc  32293  lsmcv2  32589  lcvexchlem4  32597  lcvexchlem5  32598  eqlkr  32659  paddclN  33401  pclfinN  33459  ldilcnv  33674  ldilco  33675  cdleme25dN  33917  cdlemj2  34383  tendocan  34385  erng1lem  34548  erngdvlem4-rN  34560  dihord2pre  34787  dihglblem2N  34856  dochvalr  34919  hdmap14lem12  35444  hdmap14lem13  35445  pellfundre  35723  pellfundge  35724  pellfundlb  35726  dford3lem1  35875  aomclem2  35907  hashgcdeq  36069  pwinfi3  36161  iunrelexp0  36288  iunrelexpmin1  36294  iunrelexpmin2  36298  dftrcl3  36306  cnvtrclfv  36310  trclimalb2  36312  dfrtrcl3  36319  addrcom  36822  iunconlem2  37326  ssuzfz  37566  dvmptfprod  37814  dvnprodlem3  37817  funressnfv  38623  tz6.12-afv  38669  iccpartltu  38733  iccpartgtl  38734  iccpartleu  38736  iccpartgel  38737  bgoldbst  38873  bgoldbtbnd  38898  tgblthelfgott  38902  otiunsndisjX  39000  nbuhgr  39394  nbumgr  39398  uhgrnbgr0nb  39405  uvtxanbgrvtx  39448  cusgrfilem2  39500  nnsgrp  39804  ellcoellss  40215  lindsrng01  40248  suppdm  40291  nn0sumshdiglem1  40419