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

Theorem ralrimiv 2596
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 2595 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621   A.wral 2516
This theorem is referenced by:  ralrimiva  2597  ralrimivw  2598  ralrimivv  2605  r19.27av  2652  rr19.3v  2860  rabssdv  3195  rzal  3497  trin  4063  class2seteq  4117  onmindif  4419  ralxfrALT  4490  ssorduni  4514  onminex  4535  onmindif2  4540  suceloni  4541  limuni3  4580  issref  5009  frxp  6124  poxp  6126  onfununi  6291  onnseq  6294  tfrlem12  6338  tz7.48-2  6387  oaass  6492  omass  6511  oelim2  6526  oelimcl  6531  oaabs2  6576  omabs  6578  undifixp  6785  dom2lem  6834  isinf  7009  unblem4  7045  unbnn2  7047  marypha1lem  7119  supiso  7156  ordiso2  7163  card2inf  7202  elirrv  7244  wemapwe  7333  trcl  7343  tz9.13  7396  rankval3b  7431  rankunb  7455  rankuni2b  7458  scott0  7489  dfac8alem  7589  carduniima  7656  alephsmo  7662  alephval3  7670  iunfictbso  7674  dfac3  7681  dfac5lem5  7687  dfac12r  7705  dfac12k  7706  kmlem4  7712  kmlem11  7719  cfsuc  7816  cofsmo  7828  cfsmolem  7829  coftr  7832  alephsing  7835  infpssrlem3  7864  fin23lem30  7901  isf32lem2  7913  isf32lem3  7914  isf34lem6  7939  fin1a2lem11  7969  fin1a2lem13  7971  fin1a2s  7973  axcc2lem  7995  domtriomlem  8001  axdc3lem2  8010  axdc4lem  8014  axcclem  8016  axdclem2  8080  iundom2g  8095  uniimadom  8099  cardmin  8119  alephval2  8127  alephreg  8137  fpwwe2lem12  8196  wunex2  8293  wuncval2  8302  tskwe2  8328  inar1  8330  tskuni  8338  gruun  8361  intgru  8369  grutsk1  8376  genpcl  8565  ltexprlem5  8597  suplem1pr  8609  supexpr  8611  supsrlem  8666  axpre-sup  8724  supmul1  9652  supmullem1  9653  supmul  9655  peano5nni  9682  uzind  10035  zindd  10045  uzwo  10213  uzwoOLD  10214  lbzbi  10238  xrsupsslem  10556  xrinfmsslem  10557  supxrun  10565  supxrpnf  10568  supxrunb1  10569  supxrunb2  10570  icoshftf1o  10690  flval3  10876  axdc4uzlem  10975  sqrlem1  11658  sqrlem6  11663  fsum0diag2  12175  alzdvds  12505  gcdcllem1  12617  maxprmfct  12719  unbenlem  12882  vdwlem6  12960  vdwlem10  12964  firest  13264  mrieqv2d  13468  iscatd  13502  setcmon  13846  setcepi  13847  isglbd  14148  isacs4lem  14198  acsfiindd  14207  acsmapd  14208  psss  14250  ghmrn  14623  ghmpreima  14631  cntz2ss  14735  lsmsubg  14892  efgsfo  14975  gsumzaddlem  15130  dmdprdd  15164  dprd2da  15204  imasrng  15329  isabvd  15512  issrngd  15553  islssd  15620  lbsextlem3  15840  lbsextlem4  15841  lidldvgen  15934  isphld  16485  tgcl  16634  distop  16660  indistopon  16665  pptbas  16672  toponmre  16757  opnnei  16784  neiuni  16786  neindisj2  16787  ordtrest2  16861  cnpnei  16920  cnindis  16947  cmpcld  17056  uncmp  17057  hauscmplem  17060  2ndc1stc  17104  1stcrest  17106  1stcelcls  17114  llyrest  17138  nllyrest  17139  cldllycmp  17148  txcls  17226  ptpjcn  17232  ptclsg  17236  dfac14lem  17238  xkoccn  17240  txlly  17257  txnlly  17258  ptrescn  17260  tx1stc  17271  xkoco1cn  17278  xkoco2cn  17279  xkococn  17281  xkoinjcn  17308  qtopeu  17334  hmeofval  17376  ordthmeolem  17419  isfild  17480  fbasrn  17506  trfil2  17509  flimclslem  17606  fclsrest  17646  fclscf  17647  flimfcls  17648  alexsubALTlem1  17668  alexsubALTlem2  17669  alexsubALTlem3  17670  alexsubALT  17672  divstgpopn  17729  isxmetd  17818  imasdsf1olem  17864  blcls  17979  prdsxmslem2  18002  dscmet  18022  nrmmetd  18024  reperflem  18250  reconnlem2  18259  xrge0tsms  18266  fsumcn  18301  cnheibor  18380  tchcph  18594  lmmbr  18611  caubl  18660  ivthlem1  18738  ovolctb  18776  ovoliunlem2  18789  ovolscalem1  18799  ovolicc2  18808  voliunlem3  18836  ismbfd  18922  mbfimaopnlem  18937  itg2le  19021  ellimc2  19154  c1liplem1  19270  plyeq0lem  19519  dgreq0  19573  aannenlem1  19635  pilem2  19755  cxpcn3lem  20014  scvxcvx  20207  musum  20358  dchrisum0flb  20586  ostth2lem2  20710  htthlem  21422  ocsh  21787  shintcli  21833  pjss2coi  22669  pjnormssi  22673  pjclem4  22704  pj3si  22712  pj3cor1i  22714  strlem3a  22757  strb  22763  hstrlem3a  22765  hstrbi  22771  spansncv2  22798  mdsl1i  22826  cvmdi  22829  mdexchi  22840  h1da  22854  mdsymlem6  22913  sumdmdii  22920  dmdbr5ati  22927  ballotlemimin  22990  erdszelem8  23066  cvmsss2  23142  cvmfolem  23147  eupap1  23237  rtrclreclem.min  23381  dfrtrcl2  23382  dfon2lem8  23480  dfon2lem9  23481  dfon2  23482  rdgprc  23485  trpredtr  23567  trpredmintr  23568  trpredelss  23569  dftrpred3g  23570  trpredpo  23572  trpredrec  23575  wfrlem15  23604  frr3g  23614  frrlem5b  23620  frrlem5d  23622  sltval2  23643  axfelem20  23699  axfelem21  23700  funpartfv  23823  uncum2  24441  eqfnung2  24450  repfuntw  24492  prl1  24500  prl2  24501  dstr  24503  supwlub  24606  toplat  24622  sallnei  24861  intopcoaconlem3b  24870  intopcoaconb  24872  qusp  24874  cmptdst  24900  limptlimpr2lem2  24907  lvsovso  24958  claddrvr  24980  sigadd  24981  issubrv  25004  subclrvd  25006  clsmulcv  25014  clsmulrv  25015  idsubfun  25190  cmpmor  25307  setiscat  25311  indcls2  25328  nn0prpwlem  25570  ntruni  25577  clsint2  25579  fneint  25609  reftr  25621  fnessref  25625  refssfne  25626  locfincf  25638  comppfsc  25639  neibastop1  25640  neibastop2lem  25641  sdclem2  25784  fdc  25787  seqpo  25789  prdsbnd  25849  heibor  25877  rrnequiv  25891  0idl  25982  intidl  25986  unichnidl  25988  prnc  26024  pellfundre  26298  pellfundge  26299  pellfundlb  26301  dford3lem1  26451  aomclem2  26484  frlmsslsp  26580  psgnunilem2  26750  psgnghm  26769  hashgcdeq  26849  addrcom  27013  stoweidlem35  27084  bnj518  27930  bnj1137  28037  bnj1136  28039  bnj1413  28077  bnj1417  28083  bnj60  28104  lsmcv2  28349  lcvexchlem4  28357  lcvexchlem5  28358  eqlkr  28419  paddclN  29161  pclfinN  29219  ldilcnv  29434  ldilco  29435  cdleme25dN  29675  cdlemj2  30141  tendocan  30143  erng1lem  30306  erngdvlem4-rN  30318  dihord2pre  30545  dihglblem2N  30614  dochvalr  30677  hdmap14lem12  31202  hdmap14lem13  31203
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 2520
  Copyright terms: Public domain W3C validator