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

Theorem ralrimiv 2600
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 2599 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621   A.wral 2518
This theorem is referenced by:  ralrimiva  2601  ralrimivw  2602  ralrimivv  2609  r19.27av  2656  rr19.3v  2884  rabssdv  3228  rzal  3530  trin  4097  class2seteq  4151  onmindif  4454  ralxfrALT  4525  ssorduni  4549  onminex  4570  onmindif2  4575  suceloni  4576  limuni3  4615  issref  5044  frxp  6159  poxp  6161  onfununi  6326  onnseq  6329  tfrlem12  6373  tz7.48-2  6422  oaass  6527  omass  6546  oelim2  6561  oelimcl  6566  oaabs2  6611  omabs  6613  undifixp  6820  dom2lem  6869  isinf  7044  unblem4  7080  unbnn2  7082  marypha1lem  7154  supiso  7191  ordiso2  7198  card2inf  7237  elirrv  7279  wemapwe  7368  trcl  7378  tz9.13  7431  rankval3b  7466  rankunb  7490  rankuni2b  7493  scott0  7524  dfac8alem  7624  carduniima  7691  alephsmo  7697  alephval3  7705  iunfictbso  7709  dfac3  7716  dfac5lem5  7722  dfac12r  7740  dfac12k  7741  kmlem4  7747  kmlem11  7754  cfsuc  7851  cofsmo  7863  cfsmolem  7864  coftr  7867  alephsing  7870  infpssrlem3  7899  fin23lem30  7936  isf32lem2  7948  isf32lem3  7949  isf34lem6  7974  fin1a2lem11  8004  fin1a2lem13  8006  fin1a2s  8008  axcc2lem  8030  domtriomlem  8036  axdc3lem2  8045  axdc4lem  8049  axcclem  8051  axdclem2  8115  iundom2g  8130  uniimadom  8134  cardmin  8154  alephval2  8162  alephreg  8172  fpwwe2lem12  8231  wunex2  8328  wuncval2  8337  tskwe2  8363  inar1  8365  tskuni  8373  gruun  8396  intgru  8404  grutsk1  8411  genpcl  8600  ltexprlem5  8632  suplem1pr  8644  supexpr  8646  supsrlem  8701  axpre-sup  8759  supmul1  9687  supmullem1  9688  supmul  9690  peano5nni  9717  uzind  10070  zindd  10080  uzwo  10248  uzwoOLD  10249  lbzbi  10273  xrsupsslem  10591  xrinfmsslem  10592  supxrun  10600  supxrpnf  10603  supxrunb1  10604  supxrunb2  10605  icoshftf1o  10725  flval3  10911  axdc4uzlem  11010  sqrlem1  11693  sqrlem6  11698  fsum0diag2  12210  alzdvds  12540  gcdcllem1  12652  maxprmfct  12754  unbenlem  12917  vdwlem6  12995  vdwlem10  12999  firest  13299  mrieqv2d  13503  iscatd  13537  setcmon  13881  setcepi  13882  isglbd  14183  isacs4lem  14233  acsfiindd  14242  acsmapd  14243  psss  14285  ghmrn  14658  ghmpreima  14666  cntz2ss  14770  lsmsubg  14927  efgsfo  15010  gsumzaddlem  15165  dmdprdd  15199  dprd2da  15239  imasrng  15364  isabvd  15547  issrngd  15588  islssd  15655  lbsextlem3  15875  lbsextlem4  15876  lidldvgen  15969  isphld  16520  tgcl  16669  distop  16695  indistopon  16700  pptbas  16707  toponmre  16792  opnnei  16819  neiuni  16821  neindisj2  16822  ordtrest2  16896  cnpnei  16955  cnindis  16982  cmpcld  17091  uncmp  17092  hauscmplem  17095  2ndc1stc  17139  1stcrest  17141  1stcelcls  17149  llyrest  17173  nllyrest  17174  cldllycmp  17183  txcls  17261  ptpjcn  17267  ptclsg  17271  dfac14lem  17273  xkoccn  17275  txlly  17292  txnlly  17293  ptrescn  17295  tx1stc  17306  xkoco1cn  17313  xkoco2cn  17314  xkococn  17316  xkoinjcn  17343  qtopeu  17369  hmeofval  17411  ordthmeolem  17454  isfild  17515  fbasrn  17541  trfil2  17544  flimclslem  17641  fclsrest  17681  fclscf  17682  flimfcls  17683  alexsubALTlem1  17703  alexsubALTlem2  17704  alexsubALTlem3  17705  alexsubALT  17707  divstgpopn  17764  isxmetd  17853  imasdsf1olem  17899  blcls  18014  prdsxmslem2  18037  dscmet  18057  nrmmetd  18059  reperflem  18285  reconnlem2  18294  xrge0tsms  18301  fsumcn  18336  cnheibor  18415  tchcph  18629  lmmbr  18646  caubl  18695  ivthlem1  18773  ovolctb  18811  ovoliunlem2  18824  ovolscalem1  18834  ovolicc2  18843  voliunlem3  18871  ismbfd  18957  mbfimaopnlem  18972  itg2le  19056  ellimc2  19189  c1liplem1  19305  plyeq0lem  19554  dgreq0  19608  aannenlem1  19670  pilem2  19790  cxpcn3lem  20049  scvxcvx  20242  musum  20393  dchrisum0flb  20621  ostth2lem2  20745  htthlem  21457  ocsh  21822  shintcli  21868  pjss2coi  22704  pjnormssi  22708  pjclem4  22739  pj3si  22747  pj3cor1i  22749  strlem3a  22792  strb  22798  hstrlem3a  22800  hstrbi  22806  spansncv2  22833  mdsl1i  22861  cvmdi  22864  mdexchi  22875  h1da  22889  mdsymlem6  22948  sumdmdii  22955  dmdbr5ati  22962  ballotlemimin  23025  erdszelem8  23101  cvmsss2  23177  cvmfolem  23182  eupap1  23272  rtrclreclem.min  23416  dfrtrcl2  23417  dfon2lem8  23515  dfon2lem9  23516  dfon2  23517  rdgprc  23520  trpredtr  23602  trpredmintr  23603  trpredelss  23604  dftrpred3g  23605  trpredpo  23607  trpredrec  23610  wfrlem15  23639  frr3g  23649  frrlem5b  23655  frrlem5d  23657  sltval2  23678  axfelem20  23734  axfelem21  23735  funpartfv  23858  uncum2  24476  eqfnung2  24485  repfuntw  24527  prl1  24535  prl2  24536  dstr  24538  supwlub  24641  toplat  24657  sallnei  24896  intopcoaconlem3b  24905  intopcoaconb  24907  qusp  24909  cmptdst  24935  limptlimpr2lem2  24942  lvsovso  24993  claddrvr  25015  sigadd  25016  issubrv  25039  subclrvd  25041  clsmulcv  25049  clsmulrv  25050  idsubfun  25225  cmpmor  25342  setiscat  25346  indcls2  25363  nn0prpwlem  25605  ntruni  25612  clsint2  25614  fneint  25644  reftr  25656  fnessref  25660  refssfne  25661  locfincf  25673  comppfsc  25674  neibastop1  25675  neibastop2lem  25676  sdclem2  25819  fdc  25822  seqpo  25824  prdsbnd  25884  heibor  25912  rrnequiv  25926  0idl  26017  intidl  26021  unichnidl  26023  prnc  26059  pellfundre  26333  pellfundge  26334  pellfundlb  26336  dford3lem1  26486  aomclem2  26519  frlmsslsp  26615  psgnunilem2  26785  psgnghm  26804  hashgcdeq  26884  addrcom  27048  stoweidlem35  27119  bnj518  27967  bnj1137  28074  bnj1136  28076  bnj1413  28114  bnj1417  28120  bnj60  28141  lsmcv2  28386  lcvexchlem4  28394  lcvexchlem5  28395  eqlkr  28456  paddclN  29198  pclfinN  29256  ldilcnv  29471  ldilco  29472  cdleme25dN  29712  cdlemj2  30178  tendocan  30180  erng1lem  30343  erngdvlem4-rN  30355  dihord2pre  30582  dihglblem2N  30651  dochvalr  30714  hdmap14lem12  31239  hdmap14lem13  31240
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 2523
  Copyright terms: Public domain W3C validator