MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralrimiv Unicode version

Theorem ralrimiv 2587
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
StepHypRef Expression
1 nfv 1629 . 2  |-  F/ x ph
2 ralrimiv.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
31, 2ralrimi 2586 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621   A.wral 2509
This theorem is referenced by:  ralrimiva  2588  ralrimivw  2589  ralrimivv  2596  r19.27av  2643  rr19.3v  2846  rabssdv  3174  rzal  3461  trin  4020  class2seteq  4073  onmindif  4375  ralxfrALT  4444  ssorduni  4468  onminex  4489  onmindif2  4494  suceloni  4495  limuni3  4534  issref  4963  frxp  6077  poxp  6079  onfununi  6244  onnseq  6247  tfrlem12  6291  tz7.48-2  6340  oaass  6445  omass  6464  oelim2  6479  oelimcl  6484  oaabs2  6529  omabs  6531  undifixp  6738  dom2lem  6787  isinf  6961  unblem4  6997  unbnn2  6999  marypha1lem  7070  supiso  7107  ordiso2  7114  card2inf  7153  elirrv  7195  wemapwe  7284  trcl  7294  tz9.13  7347  rankval3b  7382  rankunb  7406  rankuni2b  7409  scott0  7440  dfac8alem  7540  carduniima  7607  alephsmo  7613  alephval3  7621  iunfictbso  7625  dfac3  7632  dfac5lem5  7638  dfac12r  7656  dfac12k  7657  kmlem4  7663  kmlem11  7670  cfsuc  7767  cofsmo  7779  cfsmolem  7780  coftr  7783  alephsing  7786  infpssrlem3  7815  fin23lem30  7852  isf32lem2  7864  isf32lem3  7865  isf34lem6  7890  fin1a2lem11  7920  fin1a2lem13  7922  fin1a2s  7924  axcc2lem  7946  domtriomlem  7952  axdc3lem2  7961  axdc4lem  7965  axcclem  7967  axdclem2  8031  iundom2g  8046  uniimadom  8050  cardmin  8068  alephval2  8074  alephreg  8084  fpwwe2lem12  8143  wunex2  8240  wuncval2  8249  tskwe2  8275  inar1  8277  tskuni  8285  gruun  8308  intgru  8316  grutsk1  8323  genpcl  8512  ltexprlem5  8544  suplem1pr  8556  supexpr  8558  supsrlem  8613  axpre-sup  8671  supmul1  9599  supmullem1  9600  supmul  9602  peano5nni  9629  uzind  9982  zindd  9992  uzwo  10160  uzwoOLD  10161  lbzbi  10185  xrsupsslem  10503  xrinfmsslem  10504  supxrun  10512  supxrpnf  10515  supxrunb1  10516  supxrunb2  10517  icoshftf1o  10637  flval3  10823  axdc4uzlem  10922  sqrlem1  11605  sqrlem6  11610  fsum0diag2  12122  alzdvds  12452  gcdcllem1  12564  maxprmfct  12666  unbenlem  12829  vdwlem6  12907  vdwlem10  12911  firest  13211  iscatd  13419  setcmon  13763  setcepi  13764  isglbd  14065  isacs4lem  14115  psss  14158  ghmrn  14531  ghmpreima  14539  cntz2ss  14643  lsmsubg  14800  efgsfo  14883  gsumzaddlem  15038  dmdprdd  15072  dprd2da  15112  imasrng  15237  isabvd  15420  issrngd  15461  islssd  15528  lbsextlem3  15745  lbsextlem4  15746  lidldvgen  15839  isphld  16390  tgcl  16539  distop  16565  indistopon  16570  pptbas  16577  toponmre  16662  opnnei  16689  neiuni  16691  neindisj2  16692  ordtrest2  16766  cnpnei  16825  cnindis  16852  cmpcld  16961  uncmp  16962  hauscmplem  16965  2ndc1stc  17009  1stcrest  17011  1stcelcls  17019  llyrest  17043  nllyrest  17044  cldllycmp  17053  txcls  17131  ptpjcn  17137  ptclsg  17141  dfac14lem  17143  xkoccn  17145  txlly  17162  txnlly  17163  ptrescn  17165  tx1stc  17176  xkoco1cn  17183  xkoco2cn  17184  xkococn  17186  xkoinjcn  17213  qtopeu  17239  hmeofval  17281  ordthmeolem  17324  isfild  17385  fbasrn  17411  trfil2  17414  flimclslem  17511  fclsrest  17551  fclscf  17552  flimfcls  17553  alexsubALTlem1  17573  alexsubALTlem2  17574  alexsubALTlem3  17575  alexsubALT  17577  divstgpopn  17634  isxmetd  17723  imasdsf1olem  17769  blcls  17884  prdsxmslem2  17907  dscmet  17927  nrmmetd  17929  reperflem  18155  reconnlem2  18164  xrge0tsms  18171  fsumcn  18206  cnheibor  18285  tchcph  18499  lmmbr  18516  caubl  18565  ivthlem1  18643  ovolctb  18681  ovoliunlem2  18694  ovolscalem1  18704  ovolicc2  18713  voliunlem3  18741  ismbfd  18827  mbfimaopnlem  18842  itg2le  18926  ellimc2  19059  c1liplem1  19175  plyeq0lem  19424  dgreq0  19478  aannenlem1  19540  pilem2  19660  cxpcn3lem  19955  scvxcvx  20112  musum  20263  dchrisum0flb  20491  ostth2lem2  20615  htthlem  21327  ocsh  21692  shintcli  21738  pjss2coi  22574  pjnormssi  22578  pjclem4  22609  pj3si  22617  pj3cor1i  22619  strlem3a  22662  strb  22668  hstrlem3a  22670  hstrbi  22676  spansncv2  22703  mdsl1i  22731  cvmdi  22734  mdexchi  22745  h1da  22759  mdsymlem6  22818  sumdmdii  22825  dmdbr5ati  22832  erdszelem8  22900  cvmsss2  22976  cvmfolem  22981  eupap1  23071  rtrclreclem.min  23215  dfrtrcl2  23216  dfon2lem8  23314  dfon2lem9  23315  dfon2  23316  rdgprc  23319  trpredtr  23401  trpredmintr  23402  trpredelss  23403  dftrpred3g  23404  trpredpo  23406  trpredrec  23409  wfrlem15  23438  frr3g  23448  frrlem5b  23454  frrlem5d  23456  sltval2  23477  axfelem20  23533  axfelem21  23534  funpartfv  23657  uncum2  24275  eqfnung2  24284  repfuntw  24326  prl1  24334  prl2  24335  dstr  24337  supwlub  24440  toplat  24456  sallnei  24695  intopcoaconlem3b  24704  intopcoaconb  24706  qusp  24708  cmptdst  24734  limptlimpr2lem2  24741  lvsovso  24792  claddrvr  24814  sigadd  24815  issubrv  24838  subclrvd  24840  clsmulcv  24848  clsmulrv  24849  idsubfun  25024  cmpmor  25141  setiscat  25145  indcls2  25162  nn0prpwlem  25404  ntruni  25411  clsint2  25413  fneint  25443  reftr  25455  fnessref  25459  refssfne  25460  locfincf  25472  comppfsc  25473  neibastop1  25474  neibastop2lem  25475  sdclem2  25618  fdc  25621  seqpo  25623  prdsbnd  25683  heibor  25711  rrnequiv  25725  0idl  25816  intidl  25820  unichnidl  25822  prnc  25858  pellfundre  26132  pellfundge  26133  pellfundlb  26135  dford3lem1  26285  aomclem2  26318  frlmsslsp  26414  psgnunilem2  26584  psgnghm  26603  hashgcdeq  26683  addrcom  26847  bnj518  27607  bnj1137  27714  bnj1136  27716  bnj1413  27754  bnj1417  27760  bnj60  27781  lsmcv2  27908  lcvexchlem4  27916  lcvexchlem5  27917  eqlkr  27978  paddclN  28720  pclfinN  28778  ldilcnv  28993  ldilco  28994  cdleme25dN  29234  cdlemj2  29700  tendocan  29702  erng1lem  29865  erngdvlem4-rN  29877  dihord2pre  30104  dihglblem2N  30173  dochvalr  30236  hdmap14lem12  30761  hdmap14lem13  30762
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-nf 1540  df-ral 2513
  Copyright terms: Public domain W3C validator