Theorem ralrimiv 2965

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

Syntax hints:   -> wi 4   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

This theorem depends on definitions:  df-bi 197  df-ral 2917

This theorem is referenced by:  ralrimiva  2966  ralrimivw  2967  ralrimdv  2968  ralrimivv  2970  reximdvai  3015  r19.27v  3070  raleleq  3156  rr19.3v  3345  rabssdv  3682  rzal  4073  ssdifsn  4318  disjord  4641  disjiund  4643  trin  4763  class2seteq  4833  ralxfrALT  4887  otiunsndisj  4980  issref  5509  onmindif  5815  fnprb  6472  fntpb  6473  ssorduni  6985  onminex  7007  onmindif2  7012  suceloni  7013  limuni3  7052  frxp  7287  poxp  7289  wfrlem15  7429  onfununi  7438  onnseq  7441  tfrlem12  7485  tz7.48-2  7537  oaass  7641  omass  7660  oelim2  7675  oelimcl  7680  oaabs2  7725  omabs  7727  undifixp  7944  dom2lem  7995  isinf  8173  unblem4  8215  unbnn2  8217  marypha1lem  8339  supiso  8381  ordiso2  8420  card2inf  8460  elirrv  8504  wemapwe  8594  trcl  8604  tz9.13  8654  rankval3b  8689  rankunb  8713  rankuni2b  8716  scott0  8749  dfac8alem  8852  carduniima  8919  alephsmo  8925  alephval3  8933  iunfictbso  8937  dfac3  8944  dfac5lem5  8950  dfac12r  8968  dfac12k  8969  kmlem4  8975  kmlem11  8982  cfsuc  9079  cofsmo  9091  cfsmolem  9092  coftr  9095  alephsing  9098  infpssrlem3  9127  fin23lem30  9164  isf32lem2  9176  isf32lem3  9177  isf34lem6  9202  fin1a2lem11  9232  fin1a2lem13  9234  fin1a2s  9236  axcc2lem  9258  domtriomlem  9264  axdc3lem2  9273  axdc4lem  9277  axcclem  9279  axdclem2  9342  iundom2g  9362  uniimadom  9366  cardmin  9386  alephval2  9394  alephreg  9404  fpwwe2lem12  9463  wunex2  9560  wuncval2  9569  tskwe2  9595  inar1  9597  tskuni  9605  gruun  9628  intgru  9636  grutsk1  9643  genpcl  9830  ltexprlem5  9862  suplem1pr  9874  supexpr  9876  supsrlem  9932  axpre-sup  9990  fiminre  10972  supaddc  10990  supadd  10991  supmul1  10992  supmullem1  10993  supmul  10995  peano5nni  11023  uzind  11469  zindd  11478  uzwo  11751  lbzbi  11776  xrsupsslem  12137  xrinfmsslem  12138  supxrun  12146  supxrpnf  12148  supxrunb1  12149  supxrunb2  12150  icoshftf1o  12295  flval3  12616  axdc4uzlem  12782  ccatrn  13372  2cshw  13559  cshweqrep  13567  s3iunsndisj  13707  rtrclreclem4  13801  dfrtrcl2  13802  sqrlem1  13983  sqrlem6  13988  fsum0diag2  14515  alzdvds  15042  gcdcllem1  15221  lcmfunsnlem2lem1  15351  lcmfunsnlem2lem2  15352  maxprmfct  15421  hashgcdeq  15494  unbenlem  15612  vdwlem6  15690  vdwlem10  15694  firest  16093  mrieqv2d  16299  iscatd  16334  setcmon  16737  setcepi  16738  fullestrcsetc  16791  fullsetcestrc  16806  isglbd  17117  isacs4lem  17168  acsfiindd  17177  acsmapd  17178  psss  17214  ghmrn  17673  ghmpreima  17682  cntz2ss  17765  symgextres  17845  psgnunilem2  17915  lsmsubg  18069  efgsfo  18152  gsumzaddlem  18321  gsummptnn0fzfv  18384  dmdprdd  18398  dprd2da  18441  imasring  18619  isabvd  18820  issrngd  18861  islssd  18936  lbsextlem3  19160  lbsextlem4  19161  lidldvgen  19255  psgnghm  19926  isphld  19999  frlmsslsp  20135  mp2pm2mplem4  20614  tgcl  20773  distop  20799  indistopon  20805  pptbas  20812  toponmre  20897  opnnei  20924  neiuni  20926  neindisj2  20927  ordtrest2  21008  cnpnei  21068  cnindis  21096  cmpcld  21205  uncmp  21206  hauscmplem  21209  2ndc1stc  21254  1stcrest  21256  1stcelcls  21264  llyrest  21288  nllyrest  21289  cldllycmp  21298  reftr  21317  locfincf  21334  comppfsc  21335  txcls  21407  ptpjcn  21414  ptclsg  21418  dfac14lem  21420  xkoccn  21422  txlly  21439  txnlly  21440  ptrescn  21442  tx1stc  21453  xkoco1cn  21460  xkoco2cn  21461  xkococn  21463  xkoinjcn  21490  qtopeu  21519  hmeofval  21561  ordthmeolem  21604  isfild  21662  fbasrn  21688  trfil2  21691  flimclslem  21788  fclsrest  21828  fclscf  21829  flimfcls  21830  alexsubALTlem1  21851  alexsubALTlem2  21852  alexsubALTlem3  21853  alexsubALT  21855  qustgpopn  21923  isxmetd  22131  imasdsf1olem  22178  blcls  22311  prdsxmslem2  22334  metustfbas  22362  dscmet  22377  nrmmetd  22379  reperflem  22621  reconnlem2  22630  xrge0tsms  22637  fsumcn  22673  cnheibor  22754  tchcph  23036  lmmbr  23056  caubl  23106  ivthlem1  23220  ovolctb  23258  ovoliunlem2  23271  ovolscalem1  23281  ovolicc2  23290  voliunlem3  23320  ismbfd  23407  mbfimaopnlem  23422  itg2le  23506  ellimc2  23641  c1liplem1  23759  plyeq0lem  23966  dgreq0  24021  aannenlem1  24083  pilem2  24206  cxpcn3lem  24488  scvxcvx  24712  musum  24917  dchrisum0flb  25199  ostth2lem2  25323  numedglnl  26039  upgrreslem  26196  umgrreslem  26197  nbuhgr  26239  nbumgr  26243  uhgrnbgr0nb  26250  uvtxanbgrvtx  26293  cusgrfilem2  26352  uspgr2wlkeq  26542  wwlks  26727  rusgr0edg  26868  clwwisshclwwslem  26927  3cyclfrgrrn  27150  vdgn1frgrv3  27161  2wspmdisj  27201  numclwlk2lem2f1o  27238  frgrregord013  27253  htthlem  27774  ocsh  28142  shintcli  28188  pjss2coi  29023  pjnormssi  29027  pjclem4  29058  pj3si  29066  pj3cor1i  29068  strlem3a  29111  strb  29117  hstrlem3a  29119  hstrbi  29125  spansncv2  29152  mdsl1i  29180  cvmdi  29183  mdexchi  29194  h1da  29208  mdsymlem6  29267  sumdmdii  29274  dmdbr5ati  29281  isoun  29479  supssd  29487  infssd  29488  xrge0tsmsd  29785  ordtrest2NEW  29969  pwsiga  30193  measiun  30281  dya2iocuni  30345  bnj518  30956  bnj1137  31063  bnj1136  31065  bnj1413  31103  bnj1417  31109  bnj60  31130  erdszelem8  31180  cvmsss2  31256  cvmfolem  31261  dfon2lem8  31695  dfon2lem9  31696  dfon2  31697  rdgprc  31700  trpredtr  31730  trpredmintr  31731  trpredelss  31732  dftrpred3g  31733  trpredpo  31735  trpredrec  31738  frr3g  31779  frrlem5b  31785  frrlem5d  31787  sltval2  31809  nolesgn2ores  31825  nosupres  31853  nosupbnd2lem1  31861  scutun12  31917  nn0prpwlem  32317  ntruni  32322  clsint2  32324  fneint  32343  fnessref  32352  refssfne  32353  neibastop1  32354  neibastop2lem  32355  bj-0int  33055  bj-ismooredr2  33065  relowlpssretop  33212  heicant  33444  mblfinlem1  33446  ftc2nc  33494  sdclem2  33538  fdc  33541  seqpo  33543  prdsbnd  33592  heibor  33620  rrnequiv  33634  0idl  33824  intidl  33828  unichnidl  33830  prnc  33866  uniqsALTV  34101  lsmcv2  34316  lcvexchlem4  34324  lcvexchlem5  34325  eqlkr  34386  paddclN  35128  pclfinN  35186  ldilcnv  35401  ldilco  35402  cdleme25dN  35644  cdlemj2  36110  tendocan  36112  erng1lem  36275  erngdvlem4-rN  36287  dihord2pre  36514  dihglblem2N  36583  dochvalr  36646  hdmap14lem12  37171  hdmap14lem13  37172  pellfundre  37445  pellfundge  37446  pellfundlb  37448  dford3lem1  37593  aomclem2  37625  pwinfi3  37868  iunrelexp0  37994  iunrelexpmin1  38000  iunrelexpmin2  38004  dftrcl3  38012  cnvtrclfv  38016  trclimalb2  38018  dfrtrcl3  38025  ntrneiel2  38384  ntrneik4w  38398  ntrrn  38420  gneispa  38428  gneispb  38429  addrcom  38679  iunconnlem2  39171  ssuzfz  39565  dvmptfprod  40160  dvnprodlem3  40163  funressnfv  41208  tz6.12-afv  41253  otiunsndisjX  41298  iccpartltu  41361  iccpartgtl  41362  iccpartleu  41364  iccpartgel  41365  fargshiftf  41376  fargshiftfva  41379  sbgoldbst  41666  bgoldbtbnd  41697  tgblthelfgott  41703  tgblthelfgottOLD  41709  nnsgrp  41817  ellcoellss  42224  lindsrng01  42257  suppdm  42300  nn0sumshdiglem1  42415  setrec2fun  42439