Theorem ralrimiv 2788

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

Syntax hints:   -> wi 4   e. wcel 1755   A.wral 2705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791

This theorem depends on definitions:  df-bi 185  df-ex 1590  df-nf 1593  df-ral 2710

This theorem is referenced by:  ralrimiva  2789  ralrimivw  2790  ralrimivv  2797  r19.27av  2845  rr19.3v  3090  rabssdv  3420  rzal  3769  trin  4383  class2seteq  4448  ralxfrALT  4499  onmindif  4795  issref  5199  fnprb  5923  fnprOLD  5924  ssorduni  6386  onminex  6407  onmindif2  6412  suceloni  6413  limuni3  6452  frxp  6671  poxp  6673  onfununi  6788  onnseq  6791  tfrlem12  6834  tz7.48-2  6883  oaass  6988  omass  7007  oelim2  7022  oelimcl  7027  oaabs2  7072  omabs  7074  undifixp  7287  dom2lem  7337  isinf  7514  unblem4  7555  unbnn2  7557  marypha1lem  7671  supiso  7710  ordiso2  7717  card2inf  7758  elirrv  7800  wemapwe  7916  wemapweOLD  7917  trcl  7936  tz9.13  7986  rankval3b  8021  rankunb  8045  rankuni2b  8048  scott0  8081  dfac8alem  8187  carduniima  8254  alephsmo  8260  alephval3  8268  iunfictbso  8272  dfac3  8279  dfac5lem5  8285  dfac12r  8303  dfac12k  8304  kmlem4  8310  kmlem11  8317  cfsuc  8414  cofsmo  8426  cfsmolem  8427  coftr  8430  alephsing  8433  infpssrlem3  8462  fin23lem30  8499  isf32lem2  8511  isf32lem3  8512  isf34lem6  8537  fin1a2lem11  8567  fin1a2lem13  8569  fin1a2s  8571  axcc2lem  8593  domtriomlem  8599  axdc3lem2  8608  axdc4lem  8612  axcclem  8614  axdclem2  8677  iundom2g  8692  uniimadom  8696  cardmin  8716  alephval2  8724  alephreg  8734  fpwwe2lem12  8795  wunex2  8892  wuncval2  8901  tskwe2  8927  inar1  8929  tskuni  8937  gruun  8960  intgru  8968  grutsk1  8975  genpcl  9164  ltexprlem5  9196  suplem1pr  9208  supexpr  9210  supsrlem  9265  axpre-sup  9323  supmul1  10282  supmullem1  10283  supmul  10285  peano5nni  10312  uzind  10720  zindd  10730  uzwo  10904  uzwoOLD  10905  lbzbi  10930  xrsupsslem  11256  xrinfmsslem  11257  supxrun  11265  supxrpnf  11268  supxrunb1  11269  supxrunb2  11270  icoshftf1o  11394  flval3  11646  axdc4uzlem  11787  2cshw  12430  cshweqrep  12438  sqrlem1  12715  sqrlem6  12720  fsum0diag2  13232  alzdvds  13565  gcdcllem1  13677  maxprmfct  13781  unbenlem  13951  vdwlem6  14029  vdwlem10  14033  firest  14353  mrieqv2d  14559  iscatd  14593  setcmon  14937  setcepi  14938  isglbd  15269  isacs4lem  15320  acsfiindd  15329  acsmapd  15330  psss  15366  ghmrn  15739  ghmpreima  15747  cntz2ss  15829  symgextres  15909  psgnunilem2  15980  lsmsubg  16132  efgsfo  16215  gsumzaddlem  16387  gsumzaddlemOLD  16389  dmdprdd  16454  dprd2da  16514  imasrng  16645  isabvd  16828  issrngd  16869  islssd  16938  lbsextlem3  17162  lbsextlem4  17163  lidldvgen  17258  psgnghm  17851  isphld  17924  frlmsslsp  18064  frlmsslspOLD  18065  tgcl  18415  distop  18441  indistopon  18446  pptbas  18453  toponmre  18538  opnnei  18565  neiuni  18567  neindisj2  18568  ordtrest2  18649  cnpnei  18709  cnindis  18737  cmpcld  18846  uncmp  18847  hauscmplem  18850  2ndc1stc  18896  1stcrest  18898  1stcelcls  18906  llyrest  18930  nllyrest  18931  cldllycmp  18940  txcls  19018  ptpjcn  19025  ptclsg  19029  dfac14lem  19031  xkoccn  19033  txlly  19050  txnlly  19051  ptrescn  19053  tx1stc  19064  xkoco1cn  19071  xkoco2cn  19072  xkococn  19074  xkoinjcn  19101  qtopeu  19130  hmeofval  19172  ordthmeolem  19215  isfild  19272  fbasrn  19298  trfil2  19301  flimclslem  19398  fclsrest  19438  fclscf  19439  flimfcls  19440  alexsubALTlem1  19460  alexsubALTlem2  19461  alexsubALTlem3  19462  alexsubALT  19464  divstgpopn  19531  isxmetd  19742  imasdsf1olem  19789  blcls  19922  prdsxmslem2  19945  metustfbasOLD  19981  metustfbas  19982  dscmet  20006  nrmmetd  20008  reperflem  20236  reconnlem2  20245  xrge0tsms  20252  fsumcn  20287  cnheibor  20368  tchcph  20593  lmmbr  20610  caubl  20659  ivthlem1  20776  ovolctb  20814  ovoliunlem2  20827  ovolscalem1  20837  ovolicc2  20846  voliunlem3  20874  ismbfd  20959  mbfimaopnlem  20974  itg2le  21058  ellimc2  21193  c1liplem1  21309  plyeq0lem  21562  dgreq0  21616  aannenlem1  21678  pilem2  21801  cxpcn3lem  22069  scvxcvx  22263  musum  22415  dchrisum0flb  22643  ostth2lem2  22767  usgrares1  23145  nbusgra  23161  nbgra0nb  23162  nbgra0edg  23165  cusgrafilem2  23210  usgrasscusgra  23213  uvtxnbgravtx  23225  fargshiftf  23344  fargshiftfva  23347  eupatrl  23411  eupap1  23419  htthlem  24141  ocsh  24508  shintcli  24554  pjss2coi  25390  pjnormssi  25394  pjclem4  25425  pj3si  25433  pj3cor1i  25435  strlem3a  25478  strb  25484  hstrlem3a  25486  hstrbi  25492  spansncv2  25519  mdsl1i  25547  cvmdi  25550  mdexchi  25561  h1da  25575  mdsymlem6  25634  sumdmdii  25641  dmdbr5ati  25648  isoun  25820  supssd  25827  xrge0tsmsd  26105  ordtrest2NEW  26206  pwsiga  26426  measiun  26485  dya2iocuni  26551  erdszelem8  26933  cvmsss2  27010  cvmfolem  27015  rtrclreclem.min  27195  dfrtrcl2  27196  dfon2lem8  27449  dfon2lem9  27450  dfon2  27451  rdgprc  27454  trpredtr  27540  trpredmintr  27541  trpredelss  27542  dftrpred3g  27543  trpredpo  27545  trpredrec  27548  wfrlem15  27584  frr3g  27613  frrlem5b  27619  frrlem5d  27621  sltval2  27643  supaddc  28258  supadd  28259  heicant  28267  mblfinlem1  28269  ftc2nc  28317  nn0prpwlem  28358  ntruni  28363  clsint2  28365  fneint  28390  reftr  28402  fnessref  28406  refssfne  28407  locfincf  28419  comppfsc  28420  neibastop1  28421  neibastop2lem  28422  sdclem2  28479  fdc  28482  seqpo  28484  prdsbnd  28533  heibor  28561  rrnequiv  28575  0idl  28666  intidl  28670  unichnidl  28672  prnc  28708  pellfundre  29064  pellfundge  29065  pellfundlb  29067  dford3lem1  29217  aomclem2  29250  hashgcdeq  29408  addrcom  29573  funressnfv  29877  tz6.12-afv  29922  otiunsndisj  29975  usg2wlkeq  30132  clwwlkn0  30280  clwwisshclwwlem  30313  0egra0rgra  30392  3cyclfrgrarn  30448  vdgn1frgrav3  30464  numclwlk2lem2f1o  30541  frgraregord013  30554  ellcoellss  30675  lindsrng01  30708  snlindsntorlem  30710  iunconlem2  31370  bnj518  31578  bnj1137  31685  bnj1136  31687  bnj1413  31725  bnj1417  31731  bnj60  31752  lsmcv2  32244  lcvexchlem4  32252  lcvexchlem5  32253  eqlkr  32314  paddclN  33056  pclfinN  33114  ldilcnv  33329  ldilco  33330  cdleme25dN  33570  cdlemj2  34036  tendocan  34038  erng1lem  34201  erngdvlem4-rN  34213  dihord2pre  34440  dihglblem2N  34509  dochvalr  34572  hdmap14lem12  35097  hdmap14lem13  35098