Theorem ralrimiv 2748

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.)

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		nfv 1626	. 2 |- F/ x ph
2		ralrimiv.1	. 2 |- ( ph -> ( x e. A -> ps ) )
3	1, 2	ralrimi 2747	1 |- ( ph -> A. x e. A ps )

Syntax hints:   -> wi 4   e. wcel 1721   A.wral 2666

This theorem is referenced by:  ralrimiva  2749  ralrimivw  2750  ralrimivv  2757  r19.27av  2804  rr19.3v  3037  rabssdv  3383  rzal  3689  trin  4272  class2seteq  4328  onmindif  4630  ralxfrALT  4701  ssorduni  4725  onminex  4746  onmindif2  4751  suceloni  4752  limuni3  4791  issref  5206  fnpr  5909  fnprOLD  5910  frxp  6415  poxp  6417  onfununi  6562  onnseq  6565  tfrlem12  6609  tz7.48-2  6658  oaass  6763  omass  6782  oelim2  6797  oelimcl  6802  oaabs2  6847  omabs  6849  undifixp  7057  dom2lem  7106  isinf  7281  unblem4  7321  unbnn2  7323  marypha1lem  7396  supiso  7433  ordiso2  7440  card2inf  7479  elirrv  7521  wemapwe  7610  trcl  7620  tz9.13  7673  rankval3b  7708  rankunb  7732  rankuni2b  7735  scott0  7766  dfac8alem  7866  carduniima  7933  alephsmo  7939  alephval3  7947  iunfictbso  7951  dfac3  7958  dfac5lem5  7964  dfac12r  7982  dfac12k  7983  kmlem4  7989  kmlem11  7996  cfsuc  8093  cofsmo  8105  cfsmolem  8106  coftr  8109  alephsing  8112  infpssrlem3  8141  fin23lem30  8178  isf32lem2  8190  isf32lem3  8191  isf34lem6  8216  fin1a2lem11  8246  fin1a2lem13  8248  fin1a2s  8250  axcc2lem  8272  domtriomlem  8278  axdc3lem2  8287  axdc4lem  8291  axcclem  8293  axdclem2  8356  iundom2g  8371  uniimadom  8375  cardmin  8395  alephval2  8403  alephreg  8413  fpwwe2lem12  8472  wunex2  8569  wuncval2  8578  tskwe2  8604  inar1  8606  tskuni  8614  gruun  8637  intgru  8645  grutsk1  8652  genpcl  8841  ltexprlem5  8873  suplem1pr  8885  supexpr  8887  supsrlem  8942  axpre-sup  9000  supmul1  9929  supmullem1  9930  supmul  9932  peano5nni  9959  uzind  10317  zindd  10327  uzwo  10495  uzwoOLD  10496  lbzbi  10520  xrsupsslem  10841  xrinfmsslem  10842  supxrun  10850  supxrpnf  10853  supxrunb1  10854  supxrunb2  10855  icoshftf1o  10976  flval3  11177  axdc4uzlem  11276  sqrlem1  12003  sqrlem6  12008  fsum0diag2  12521  alzdvds  12854  gcdcllem1  12966  maxprmfct  13068  unbenlem  13231  vdwlem6  13309  vdwlem10  13313  firest  13615  mrieqv2d  13819  iscatd  13853  setcmon  14197  setcepi  14198  isglbd  14499  isacs4lem  14549  acsfiindd  14558  acsmapd  14559  psss  14601  ghmrn  14974  ghmpreima  14982  cntz2ss  15086  lsmsubg  15243  efgsfo  15326  gsumzaddlem  15481  dmdprdd  15515  dprd2da  15555  imasrng  15680  isabvd  15863  issrngd  15904  islssd  15967  lbsextlem3  16187  lbsextlem4  16188  lidldvgen  16281  isphld  16840  tgcl  16989  distop  17015  indistopon  17020  pptbas  17027  toponmre  17112  opnnei  17139  neiuni  17141  neindisj2  17142  ordtrest2  17222  cnpnei  17282  cnindis  17310  cmpcld  17419  uncmp  17420  hauscmplem  17423  2ndc1stc  17467  1stcrest  17469  1stcelcls  17477  llyrest  17501  nllyrest  17502  cldllycmp  17511  txcls  17589  ptpjcn  17596  ptclsg  17600  dfac14lem  17602  xkoccn  17604  txlly  17621  txnlly  17622  ptrescn  17624  tx1stc  17635  xkoco1cn  17642  xkoco2cn  17643  xkococn  17645  xkoinjcn  17672  qtopeu  17701  hmeofval  17743  ordthmeolem  17786  isfild  17843  fbasrn  17869  trfil2  17872  flimclslem  17969  fclsrest  18009  fclscf  18010  flimfcls  18011  alexsubALTlem1  18031  alexsubALTlem2  18032  alexsubALTlem3  18033  alexsubALT  18035  divstgpopn  18102  isxmetd  18309  imasdsf1olem  18356  blcls  18489  prdsxmslem2  18512  metustfbasOLD  18548  metustfbas  18549  dscmet  18573  nrmmetd  18575  reperflem  18802  reconnlem2  18811  xrge0tsms  18818  fsumcn  18853  cnheibor  18933  tchcph  19147  lmmbr  19164  caubl  19213  ivthlem1  19301  ovolctb  19339  ovoliunlem2  19352  ovolscalem1  19362  ovolicc2  19371  voliunlem3  19399  ismbfd  19485  mbfimaopnlem  19500  itg2le  19584  ellimc2  19717  c1liplem1  19833  plyeq0lem  20082  dgreq0  20136  aannenlem1  20198  pilem2  20321  cxpcn3lem  20584  scvxcvx  20777  musum  20929  dchrisum0flb  21157  ostth2lem2  21281  usgrares1  21377  nbusgra  21393  nbgra0nb  21394  nbgra0edg  21397  cusgrafilem2  21442  usgrasscusgra  21445  uvtxnbgravtx  21457  fargshiftf  21576  fargshiftfva  21579  eupatrl  21643  eupap1  21651  htthlem  22373  ocsh  22738  shintcli  22784  pjss2coi  23620  pjnormssi  23624  pjclem4  23655  pj3si  23663  pj3cor1i  23665  strlem3a  23708  strb  23714  hstrlem3a  23716  hstrbi  23722  spansncv2  23749  mdsl1i  23777  cvmdi  23780  mdexchi  23791  h1da  23805  mdsymlem6  23864  sumdmdii  23871  dmdbr5ati  23878  isoun  24042  supssd  24051  xrge0tsmsd  24176  pwsiga  24466  measiun  24525  dya2iocuni  24586  erdszelem8  24837  cvmsss2  24914  cvmfolem  24919  rtrclreclem.min  25100  dfrtrcl2  25101  dfon2lem8  25360  dfon2lem9  25361  dfon2  25362  rdgprc  25365  trpredtr  25447  trpredmintr  25448  trpredelss  25449  dftrpred3g  25450  trpredpo  25452  trpredrec  25455  wfrlem15  25484  frr3g  25494  frrlem5b  25500  frrlem5d  25502  sltval2  25524  supaddc  26137  supadd  26138  mblfinlem  26143  nn0prpwlem  26215  ntruni  26220  clsint2  26222  fneint  26247  reftr  26259  fnessref  26263  refssfne  26264  locfincf  26276  comppfsc  26277  neibastop1  26278  neibastop2lem  26279  sdclem2  26336  fdc  26339  seqpo  26341  prdsbnd  26392  heibor  26420  rrnequiv  26434  0idl  26525  intidl  26529  unichnidl  26531  prnc  26567  pellfundre  26834  pellfundge  26835  pellfundlb  26837  dford3lem1  26987  aomclem2  27020  frlmsslsp  27116  psgnunilem2  27286  psgnghm  27305  hashgcdeq  27385  addrcom  27547  funressnfv  27859  tz6.12-afv  27904  otiunsndisj  27954  3cyclfrgrarn  28117  bnj518  28963  bnj1137  29070  bnj1136  29072  bnj1413  29110  bnj1417  29116  bnj60  29137  lsmcv2  29512  lcvexchlem4  29520  lcvexchlem5  29521  eqlkr  29582  paddclN  30324  pclfinN  30382  ldilcnv  30597  ldilco  30598  cdleme25dN  30838  cdlemj2  31304  tendocan  31306  erng1lem  31469  erngdvlem4-rN  31481  dihord2pre  31708  dihglblem2N  31777  dochvalr  31840  hdmap14lem12  32365  hdmap14lem13  32366

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757

This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551  df-ral 2671