Theorem ralrimiv 2815

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

Syntax hints:   -> wi 4   e. wcel 1842   A.wral 2753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725

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

This theorem is referenced by:  ralrimiva  2817  ralrimivw  2818  ralrimdv  2819  ralrimivv  2823  reximdvai  2875  r19.27v  2939  rr19.3v  3190  rabssdv  3518  rzal  3874  trin  4498  class2seteq  4561  ralxfrALT  4609  otiunsndisj  4695  issref  5200  onmindif  5498  fnprb  6109  ssorduni  6602  onminex  6624  onmindif2  6629  suceloni  6630  limuni3  6669  frxp  6893  poxp  6895  wfrlem15  7034  onfununi  7044  onnseq  7047  tfrlem12  7091  tz7.48-2  7143  oaass  7246  omass  7265  oelim2  7280  oelimcl  7285  oaabs2  7330  omabs  7332  undifixp  7542  dom2lem  7592  isinf  7767  unblem4  7808  unbnn2  7810  marypha1lem  7926  supiso  7966  ordiso2  7973  card2inf  8014  elirrv  8056  wemapwe  8170  wemapweOLD  8171  trcl  8190  tz9.13  8240  rankval3b  8275  rankunb  8299  rankuni2b  8302  scott0  8335  dfac8alem  8441  carduniima  8508  alephsmo  8514  alephval3  8522  iunfictbso  8526  dfac3  8533  dfac5lem5  8539  dfac12r  8557  dfac12k  8558  kmlem4  8564  kmlem11  8571  cfsuc  8668  cofsmo  8680  cfsmolem  8681  coftr  8684  alephsing  8687  infpssrlem3  8716  fin23lem30  8753  isf32lem2  8765  isf32lem3  8766  isf34lem6  8791  fin1a2lem11  8821  fin1a2lem13  8823  fin1a2s  8825  axcc2lem  8847  domtriomlem  8853  axdc3lem2  8862  axdc4lem  8866  axcclem  8868  axdclem2  8931  iundom2g  8946  uniimadom  8950  cardmin  8970  alephval2  8978  alephreg  8988  fpwwe2lem12  9048  wunex2  9145  wuncval2  9154  tskwe2  9180  inar1  9182  tskuni  9190  gruun  9213  intgru  9221  grutsk1  9228  genpcl  9415  ltexprlem5  9447  suplem1pr  9459  supexpr  9461  supsrlem  9517  axpre-sup  9575  supmul1  10547  supmullem1  10548  supmul  10550  peano5nni  10578  uzind  10994  zindd  11003  uzwo  11189  lbzbi  11214  xrsupsslem  11550  xrinfmsslem  11551  supxrun  11559  supxrpnf  11562  supxrunb1  11563  supxrunb2  11564  icoshftf1o  11695  flval3  11986  axdc4uzlem  12131  ccatrn  12658  2cshw  12835  cshweqrep  12843  rtrclreclem4  13041  dfrtrcl2  13042  sqrlem1  13223  sqrlem6  13228  fsum0diag2  13747  alzdvds  14243  gcdcllem1  14356  maxprmfct  14461  unbenlem  14633  vdwlem6  14711  vdwlem10  14715  firest  15045  mrieqv2d  15251  iscatd  15285  setcmon  15688  setcepi  15689  fullestrcsetc  15742  fullsetcestrc  15757  isglbd  16069  isacs4lem  16120  acsfiindd  16129  acsmapd  16130  psss  16166  ghmrn  16602  ghmpreima  16610  cntz2ss  16692  symgextres  16772  psgnunilem2  16842  lsmsubg  16996  efgsfo  17079  gsumzaddlem  17256  gsumzaddlemOLD  17258  gsummptnn0fzfv  17334  dmdprdd  17348  dprd2da  17409  imasring  17586  isabvd  17787  issrngd  17828  islssd  17900  lbsextlem3  18124  lbsextlem4  18125  lidldvgen  18221  psgnghm  18912  isphld  18985  frlmsslsp  19121  mp2pm2mplem4  19600  tgcl  19761  distop  19787  indistopon  19792  pptbas  19799  toponmre  19885  opnnei  19912  neiuni  19914  neindisj2  19915  ordtrest2  19996  cnpnei  20056  cnindis  20084  cmpcld  20193  uncmp  20194  hauscmplem  20197  2ndc1stc  20242  1stcrest  20244  1stcelcls  20252  llyrest  20276  nllyrest  20277  cldllycmp  20286  reftr  20305  locfincf  20322  comppfsc  20323  txcls  20395  ptpjcn  20402  ptclsg  20406  dfac14lem  20408  xkoccn  20410  txlly  20427  txnlly  20428  ptrescn  20430  tx1stc  20441  xkoco1cn  20448  xkoco2cn  20449  xkococn  20451  xkoinjcn  20478  qtopeu  20507  hmeofval  20549  ordthmeolem  20592  isfild  20649  fbasrn  20675  trfil2  20678  flimclslem  20775  fclsrest  20815  fclscf  20816  flimfcls  20817  alexsubALTlem1  20837  alexsubALTlem2  20838  alexsubALTlem3  20839  alexsubALT  20841  qustgpopn  20908  isxmetd  21119  imasdsf1olem  21166  blcls  21299  prdsxmslem2  21322  metustfbasOLD  21358  metustfbas  21359  dscmet  21383  nrmmetd  21385  reperflem  21613  reconnlem2  21622  xrge0tsms  21629  fsumcn  21664  cnheibor  21745  tchcph  21970  lmmbr  21987  caubl  22036  ivthlem1  22153  ovolctb  22191  ovoliunlem2  22204  ovolscalem1  22214  ovolicc2  22223  voliunlem3  22252  ismbfd  22337  mbfimaopnlem  22352  itg2le  22436  ellimc2  22571  c1liplem1  22687  plyeq0lem  22897  dgreq0  22952  aannenlem1  23014  pilem2  23137  cxpcn3lem  23415  scvxcvx  23639  musum  23846  dchrisum0flb  24074  ostth2lem2  24198  usgrares1  24814  nbusgra  24832  nbgra0nb  24833  nbgra0edg  24836  cusgrafilem2  24884  usgrasscusgra  24887  uvtxnbgravtx  24899  fargshiftf  25040  fargshiftfva  25043  usg2wlkeq  25112  clwwlkn0  25178  clwwisshclwwlem  25210  0egra0rgra  25340  eupatrl  25372  eupap1  25380  3cyclfrgrarn  25417  vdgn1frgrav3  25432  2spotiundisj  25466  numclwlk2lem2f1o  25509  frgraregord013  25522  htthlem  26234  ocsh  26601  shintcli  26647  pjss2coi  27482  pjnormssi  27486  pjclem4  27517  pj3si  27525  pj3cor1i  27527  strlem3a  27570  strb  27576  hstrlem3a  27578  hstrbi  27584  spansncv2  27611  mdsl1i  27639  cvmdi  27642  mdexchi  27653  h1da  27667  mdsymlem6  27726  sumdmdii  27733  dmdbr5ati  27740  isoun  27950  supssd  27958  xrge0tsmsd  28214  ordtrest2NEW  28344  pwsiga  28564  measiun  28652  dya2iocuni  28717  bnj518  29258  bnj1137  29365  bnj1136  29367  bnj1413  29405  bnj1417  29411  bnj60  29432  erdszelem8  29482  cvmsss2  29558  cvmfolem  29563  dfon2lem8  29996  dfon2lem9  29997  dfon2  29998  rdgprc  30001  trpredtr  30031  trpredmintr  30032  trpredelss  30033  dftrpred3g  30034  trpredpo  30036  trpredrec  30039  frr3g  30073  frrlem5b  30079  frrlem5d  30081  sltval2  30103  nn0prpwlem  30537  ntruni  30542  clsint2  30544  fneint  30563  fnessref  30572  refssfne  30573  neibastop1  30574  neibastop2lem  30575  supaddc  31393  supadd  31394  heicant  31401  mblfinlem1  31403  ftc2nc  31452  sdclem2  31497  fdc  31500  seqpo  31502  prdsbnd  31551  heibor  31579  rrnequiv  31593  0idl  31684  intidl  31688  unichnidl  31690  prnc  31726  lsmcv2  32027  lcvexchlem4  32035  lcvexchlem5  32036  eqlkr  32097  paddclN  32839  pclfinN  32897  ldilcnv  33112  ldilco  33113  cdleme25dN  33355  cdlemj2  33821  tendocan  33823  erng1lem  33986  erngdvlem4-rN  33998  dihord2pre  34225  dihglblem2N  34294  dochvalr  34357  hdmap14lem12  34882  hdmap14lem13  34883  pellfundre  35158  pellfundge  35159  pellfundlb  35161  dford3lem1  35310  aomclem2  35343  hashgcdeq  35502  pwinfi3  35594  iunrelexp0  35661  iunrelexpmin1  35667  iunrelexpmin2  35671  dftrcl3  35679  cnvtrclfv  35683  trclimalb2  35685  dfrtrcl3  35692  addrcom  36212  iunconlem2  36746  dvmptfprod  37091  dvnprodlem3  37094  funressnfv  37562  tz6.12-afv  37607  iccpartltu  37673  iccpartgtl  37674  iccpartleu  37676  iccpartgel  37677  bgoldbst  37813  bgoldbtbnd  37838  otiunsndisjX  37915  nnsgrp  38115  ellcoellss  38528  lindsrng01  38561  suppdm  38604  nn0sumshdiglem1  38733