Theorem ralrimiv 2835

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

Syntax hints:   -> wi 4   e. wcel 1867   A.wral 2773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748

This theorem depends on definitions:  df-bi 188  df-ral 2778

This theorem is referenced by:  ralrimiva  2837  ralrimivw  2838  ralrimdv  2839  ralrimivv  2843  reximdvai  2895  r19.27v  2959  rr19.3v  3210  rabssdv  3538  rzal  3896  trin  4522  class2seteq  4585  ralxfrALT  4633  otiunsndisj  4719  issref  5225  onmindif  5523  fnprb  6130  ssorduni  6618  onminex  6640  onmindif2  6645  suceloni  6646  limuni3  6685  frxp  6909  poxp  6911  wfrlem15  7050  onfununi  7060  onnseq  7063  tfrlem12  7107  tz7.48-2  7159  oaass  7262  omass  7281  oelim2  7296  oelimcl  7301  oaabs2  7346  omabs  7348  undifixp  7558  dom2lem  7608  isinf  7783  unblem4  7824  unbnn2  7826  marypha1lem  7945  supiso  7989  ordiso2  8028  card2inf  8068  elirrv  8110  wemapwe  8199  trcl  8209  tz9.13  8259  rankval3b  8294  rankunb  8318  rankuni2b  8321  scott0  8354  dfac8alem  8456  carduniima  8523  alephsmo  8529  alephval3  8537  iunfictbso  8541  dfac3  8548  dfac5lem5  8554  dfac12r  8572  dfac12k  8573  kmlem4  8579  kmlem11  8586  cfsuc  8683  cofsmo  8695  cfsmolem  8696  coftr  8699  alephsing  8702  infpssrlem3  8731  fin23lem30  8768  isf32lem2  8780  isf32lem3  8781  isf34lem6  8806  fin1a2lem11  8836  fin1a2lem13  8838  fin1a2s  8840  axcc2lem  8862  domtriomlem  8868  axdc3lem2  8877  axdc4lem  8881  axcclem  8883  axdclem2  8946  iundom2g  8961  uniimadom  8965  cardmin  8985  alephval2  8993  alephreg  9003  fpwwe2lem12  9062  wunex2  9159  wuncval2  9168  tskwe2  9194  inar1  9196  tskuni  9204  gruun  9227  intgru  9235  grutsk1  9242  genpcl  9429  ltexprlem5  9461  suplem1pr  9473  supexpr  9475  supsrlem  9531  axpre-sup  9589  fiminre  10551  supaddc  10570  supadd  10571  supmul1  10572  supmullem1  10573  supmul  10575  peano5nni  10608  uzind  11023  zindd  11032  uzwo  11218  lbzbi  11248  xrsupsslem  11588  xrinfmsslem  11589  supxrun  11597  supxrpnf  11600  supxrunb1  11601  supxrunb2  11602  icoshftf1o  11749  flval3  12043  axdc4uzlem  12188  ccatrn  12716  2cshw  12893  cshweqrep  12901  rtrclreclem4  13103  dfrtrcl2  13104  sqrlem1  13285  sqrlem6  13290  fsum0diag2  13822  alzdvds  14333  gcdcllem1  14451  lcmfunsnlem2lem1  14589  lcmfunsnlem2lem2  14590  maxprmfct  14630  unbenlem  14830  vdwlem6  14914  vdwlem10  14918  firest  15309  mrieqv2d  15523  iscatd  15557  setcmon  15960  setcepi  15961  fullestrcsetc  16014  fullsetcestrc  16029  isglbd  16341  isacs4lem  16392  acsfiindd  16401  acsmapd  16402  psss  16438  ghmrn  16874  ghmpreima  16882  cntz2ss  16964  symgextres  17044  psgnunilem2  17114  lsmsubg  17284  efgsfo  17367  gsumzaddlem  17532  gsummptnn0fzfv  17595  dmdprdd  17609  dprd2da  17653  imasring  17825  isabvd  18026  issrngd  18067  islssd  18137  lbsextlem3  18361  lbsextlem4  18362  lidldvgen  18457  psgnghm  19125  isphld  19198  frlmsslsp  19331  mp2pm2mplem4  19810  tgcl  19962  distop  19988  indistopon  19993  pptbas  20000  toponmre  20086  opnnei  20113  neiuni  20115  neindisj2  20116  ordtrest2  20197  cnpnei  20257  cnindis  20285  cmpcld  20394  uncmp  20395  hauscmplem  20398  2ndc1stc  20443  1stcrest  20445  1stcelcls  20453  llyrest  20477  nllyrest  20478  cldllycmp  20487  reftr  20506  locfincf  20523  comppfsc  20524  txcls  20596  ptpjcn  20603  ptclsg  20607  dfac14lem  20609  xkoccn  20611  txlly  20628  txnlly  20629  ptrescn  20631  tx1stc  20642  xkoco1cn  20649  xkoco2cn  20650  xkococn  20652  xkoinjcn  20679  qtopeu  20708  hmeofval  20750  ordthmeolem  20793  isfild  20850  fbasrn  20876  trfil2  20879  flimclslem  20976  fclsrest  21016  fclscf  21017  flimfcls  21018  alexsubALTlem1  21039  alexsubALTlem2  21040  alexsubALTlem3  21041  alexsubALT  21043  qustgpopn  21111  isxmetd  21318  imasdsf1olem  21365  blcls  21498  prdsxmslem2  21521  metustfbas  21549  dscmet  21564  nrmmetd  21566  reperflem  21813  reconnlem2  21822  xrge0tsms  21829  fsumcn  21879  cnheibor  21960  tchcph  22188  lmmbr  22205  caubl  22254  ivthlem1  22379  ovolctb  22420  ovoliunlem2  22433  ovolscalem1  22443  ovolicc2  22453  voliunlem3  22482  ismbfd  22573  mbfimaopnlem  22588  itg2le  22674  ellimc2  22809  c1liplem1  22925  plyeq0lem  23141  dgreq0  23196  aannenlem1  23261  pilem2  23384  pilem2OLD  23385  cxpcn3lem  23664  scvxcvx  23888  musum  24097  dchrisum0flb  24325  ostth2lem2  24449  usgrares1  25114  nbusgra  25132  nbgra0nb  25133  nbgra0edg  25136  cusgrafilem2  25184  usgrasscusgra  25187  uvtxnbgravtx  25199  fargshiftf  25340  fargshiftfva  25343  usg2wlkeq  25412  clwwlkn0  25478  clwwisshclwwlem  25510  0egra0rgra  25640  eupatrl  25672  eupap1  25680  3cyclfrgrarn  25717  vdgn1frgrav3  25732  2spotiundisj  25766  numclwlk2lem2f1o  25809  frgraregord013  25822  htthlem  26546  ocsh  26912  shintcli  26958  pjss2coi  27793  pjnormssi  27797  pjclem4  27828  pj3si  27836  pj3cor1i  27838  strlem3a  27881  strb  27887  hstrlem3a  27889  hstrbi  27895  spansncv2  27922  mdsl1i  27950  cvmdi  27953  mdexchi  27964  h1da  27978  mdsymlem6  28037  sumdmdii  28044  dmdbr5ati  28051  isoun  28263  supssd  28271  infssd  28272  xrge0tsmsd  28537  ordtrest2NEW  28718  pwsiga  28941  measiun  29029  dya2iocuni  29094  bnj518  29686  bnj1137  29793  bnj1136  29795  bnj1413  29833  bnj1417  29839  bnj60  29860  erdszelem8  29910  cvmsss2  29986  cvmfolem  29991  dfon2lem8  30424  dfon2lem9  30425  dfon2  30426  rdgprc  30429  trpredtr  30459  trpredmintr  30460  trpredelss  30461  dftrpred3g  30462  trpredpo  30464  trpredrec  30467  frr3g  30501  frrlem5b  30507  frrlem5d  30509  sltval2  30531  nn0prpwlem  30964  ntruni  30969  clsint2  30971  fneint  30990  fnessref  30999  refssfne  31000  neibastop1  31001  neibastop2lem  31002  relowlpssretop  31702  heicant  31883  mblfinlem1  31885  ftc2nc  31934  sdclem2  31979  fdc  31982  seqpo  31984  prdsbnd  32033  heibor  32061  rrnequiv  32075  0idl  32166  intidl  32170  unichnidl  32172  prnc  32208  lsmcv2  32508  lcvexchlem4  32516  lcvexchlem5  32517  eqlkr  32578  paddclN  33320  pclfinN  33378  ldilcnv  33593  ldilco  33594  cdleme25dN  33836  cdlemj2  34302  tendocan  34304  erng1lem  34467  erngdvlem4-rN  34479  dihord2pre  34706  dihglblem2N  34775  dochvalr  34838  hdmap14lem12  35363  hdmap14lem13  35364  pellfundre  35643  pellfundge  35644  pellfundlb  35646  dford3lem1  35795  aomclem2  35827  hashgcdeq  35989  pwinfi3  36081  iunrelexp0  36148  iunrelexpmin1  36154  iunrelexpmin2  36158  dftrcl3  36166  cnvtrclfv  36170  trclimalb2  36172  dfrtrcl3  36179  addrcom  36680  iunconlem2  37187  dvmptfprod  37607  dvnprodlem3  37610  funressnfv  38250  tz6.12-afv  38295  iccpartltu  38359  iccpartgtl  38360  iccpartleu  38362  iccpartgel  38363  bgoldbst  38499  bgoldbtbnd  38524  tgblthelfgott  38528  otiunsndisjX  38616  nnsgrp  38879  ellcoellss  39292  lindsrng01  39325  suppdm  39368  nn0sumshdiglem1  39497