Theorem ralrimiv 2855

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

Syntax hints:   -> wi 4   e. wcel 1804   A.wral 2793

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691

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

This theorem is referenced by:  ralrimiva  2857  ralrimivw  2858  ralrimdv  2859  ralrimivv  2863  reximdvai  2915  r19.27av  2976  rr19.3v  3227  rabssdv  3565  rzal  3916  trin  4540  class2seteq  4605  ralxfrALT  4656  otiunsndisj  4743  onmindif  4957  issref  5370  fnprb  6114  fnprOLD  6115  ssorduni  6606  onminex  6627  onmindif2  6632  suceloni  6633  limuni3  6672  frxp  6895  poxp  6897  onfununi  7014  onnseq  7017  tfrlem12  7060  tz7.48-2  7109  oaass  7212  omass  7231  oelim2  7246  oelimcl  7251  oaabs2  7296  omabs  7298  undifixp  7507  dom2lem  7557  isinf  7735  unblem4  7777  unbnn2  7779  marypha1lem  7895  supiso  7936  ordiso2  7943  card2inf  7984  elirrv  8026  wemapwe  8142  wemapweOLD  8143  trcl  8162  tz9.13  8212  rankval3b  8247  rankunb  8271  rankuni2b  8274  scott0  8307  dfac8alem  8413  carduniima  8480  alephsmo  8486  alephval3  8494  iunfictbso  8498  dfac3  8505  dfac5lem5  8511  dfac12r  8529  dfac12k  8530  kmlem4  8536  kmlem11  8543  cfsuc  8640  cofsmo  8652  cfsmolem  8653  coftr  8656  alephsing  8659  infpssrlem3  8688  fin23lem30  8725  isf32lem2  8737  isf32lem3  8738  isf34lem6  8763  fin1a2lem11  8793  fin1a2lem13  8795  fin1a2s  8797  axcc2lem  8819  domtriomlem  8825  axdc3lem2  8834  axdc4lem  8838  axcclem  8840  axdclem2  8903  iundom2g  8918  uniimadom  8922  cardmin  8942  alephval2  8950  alephreg  8960  fpwwe2lem12  9022  wunex2  9119  wuncval2  9128  tskwe2  9154  inar1  9156  tskuni  9164  gruun  9187  intgru  9195  grutsk1  9202  genpcl  9389  ltexprlem5  9421  suplem1pr  9433  supexpr  9435  supsrlem  9491  axpre-sup  9549  supmul1  10515  supmullem1  10516  supmul  10518  peano5nni  10546  uzind  10961  zindd  10971  uzwo  11154  uzwoOLD  11155  lbzbi  11180  xrsupsslem  11508  xrinfmsslem  11509  supxrun  11517  supxrpnf  11520  supxrunb1  11521  supxrunb2  11522  icoshftf1o  11653  flval3  11932  axdc4uzlem  12073  ccatrn  12587  2cshw  12762  cshweqrep  12770  sqrlem1  13057  sqrlem6  13062  fsum0diag2  13579  alzdvds  14017  gcdcllem1  14130  maxprmfct  14235  unbenlem  14407  vdwlem6  14485  vdwlem10  14489  firest  14811  mrieqv2d  15017  iscatd  15051  setcmon  15392  setcepi  15393  isglbd  15725  isacs4lem  15776  acsfiindd  15785  acsmapd  15786  psss  15822  ghmrn  16258  ghmpreima  16266  cntz2ss  16348  symgextres  16428  psgnunilem2  16498  lsmsubg  16652  efgsfo  16735  gsumzaddlem  16912  gsumzaddlemOLD  16914  gsummptnn0fzfv  16994  dmdprdd  17008  dprd2da  17069  imasring  17246  isabvd  17447  issrngd  17488  islssd  17560  lbsextlem3  17784  lbsextlem4  17785  lidldvgen  17881  psgnghm  18593  isphld  18666  frlmsslsp  18806  frlmsslspOLD  18807  mp2pm2mplem4  19287  tgcl  19448  distop  19474  indistopon  19479  pptbas  19486  toponmre  19571  opnnei  19598  neiuni  19600  neindisj2  19601  ordtrest2  19682  cnpnei  19742  cnindis  19770  cmpcld  19879  uncmp  19880  hauscmplem  19883  2ndc1stc  19929  1stcrest  19931  1stcelcls  19939  llyrest  19963  nllyrest  19964  cldllycmp  19973  reftr  19992  locfincf  20009  comppfsc  20010  txcls  20082  ptpjcn  20089  ptclsg  20093  dfac14lem  20095  xkoccn  20097  txlly  20114  txnlly  20115  ptrescn  20117  tx1stc  20128  xkoco1cn  20135  xkoco2cn  20136  xkococn  20138  xkoinjcn  20165  qtopeu  20194  hmeofval  20236  ordthmeolem  20279  isfild  20336  fbasrn  20362  trfil2  20365  flimclslem  20462  fclsrest  20502  fclscf  20503  flimfcls  20504  alexsubALTlem1  20524  alexsubALTlem2  20525  alexsubALTlem3  20526  alexsubALT  20528  qustgpopn  20595  isxmetd  20806  imasdsf1olem  20853  blcls  20986  prdsxmslem2  21009  metustfbasOLD  21045  metustfbas  21046  dscmet  21070  nrmmetd  21072  reperflem  21300  reconnlem2  21309  xrge0tsms  21316  fsumcn  21351  cnheibor  21432  tchcph  21657  lmmbr  21674  caubl  21723  ivthlem1  21840  ovolctb  21878  ovoliunlem2  21891  ovolscalem1  21901  ovolicc2  21910  voliunlem3  21939  ismbfd  22024  mbfimaopnlem  22039  itg2le  22123  ellimc2  22258  c1liplem1  22374  plyeq0lem  22584  dgreq0  22638  aannenlem1  22700  pilem2  22823  cxpcn3lem  23097  scvxcvx  23291  musum  23443  dchrisum0flb  23671  ostth2lem2  23795  usgrares1  24386  nbusgra  24404  nbgra0nb  24405  nbgra0edg  24408  cusgrafilem2  24456  usgrasscusgra  24459  uvtxnbgravtx  24471  fargshiftf  24612  fargshiftfva  24615  usg2wlkeq  24684  clwwlkn0  24750  clwwisshclwwlem  24782  0egra0rgra  24912  eupatrl  24944  eupap1  24952  3cyclfrgrarn  24989  vdgn1frgrav3  25004  2spotiundisj  25038  numclwlk2lem2f1o  25081  frgraregord013  25094  htthlem  25810  ocsh  26177  shintcli  26223  pjss2coi  27059  pjnormssi  27063  pjclem4  27094  pj3si  27102  pj3cor1i  27104  strlem3a  27147  strb  27153  hstrlem3a  27155  hstrbi  27161  spansncv2  27188  mdsl1i  27216  cvmdi  27219  mdexchi  27230  h1da  27244  mdsymlem6  27303  sumdmdii  27310  dmdbr5ati  27317  isoun  27496  supssd  27503  xrge0tsmsd  27752  ordtrest2NEW  27882  pwsiga  28107  measiun  28166  dya2iocuni  28231  erdszelem8  28619  cvmsss2  28696  cvmfolem  28701  rtrclreclem.min  29047  dfrtrcl2  29048  dfon2lem8  29197  dfon2lem9  29198  dfon2  29199  rdgprc  29202  trpredtr  29288  trpredmintr  29289  trpredelss  29290  dftrpred3g  29291  trpredpo  29293  trpredrec  29296  wfrlem15  29332  frr3g  29361  frrlem5b  29367  frrlem5d  29369  sltval2  29391  supaddc  30016  supadd  30017  heicant  30024  mblfinlem1  30026  ftc2nc  30074  nn0prpwlem  30115  ntruni  30120  clsint2  30122  fneint  30141  fnessref  30150  refssfne  30151  neibastop1  30152  neibastop2lem  30153  sdclem2  30210  fdc  30213  seqpo  30215  prdsbnd  30264  heibor  30292  rrnequiv  30306  0idl  30397  intidl  30401  unichnidl  30403  prnc  30439  pellfundre  30792  pellfundge  30793  pellfundlb  30795  dford3lem1  30943  aomclem2  30976  hashgcdeq  31134  addrcom  31338  funressnfv  32051  tz6.12-afv  32096  otiunsndisjX  32139  nnsgrp  32342  ellcoellss  32771  lindsrng01  32804  iunconlem2  33468  bnj518  33677  bnj1137  33784  bnj1136  33786  bnj1413  33824  bnj1417  33830  bnj60  33851  lsmcv2  34494  lcvexchlem4  34502  lcvexchlem5  34503  eqlkr  34564  paddclN  35306  pclfinN  35364  ldilcnv  35579  ldilco  35580  cdleme25dN  35822  cdlemj2  36288  tendocan  36290  erng1lem  36453  erngdvlem4-rN  36465  dihord2pre  36692  dihglblem2N  36761  dochvalr  36824  hdmap14lem12  37349  hdmap14lem13  37350  pwinfi3  37451