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

Theorem ralrimiv 2638
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 1609 . 2  |-  F/ x ph
2 ralrimiv.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
31, 2ralrimi 2637 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   A.wral 2556
This theorem is referenced by:  ralrimiva  2639  ralrimivw  2640  ralrimivv  2647  r19.27av  2694  rr19.3v  2922  rabssdv  3266  rzal  3568  trin  4139  class2seteq  4195  onmindif  4498  ralxfrALT  4569  ssorduni  4593  onminex  4614  onmindif2  4619  suceloni  4620  limuni3  4659  issref  5072  frxp  6241  poxp  6243  onfununi  6374  onnseq  6377  tfrlem12  6421  tz7.48-2  6470  oaass  6575  omass  6594  oelim2  6609  oelimcl  6614  oaabs2  6659  omabs  6661  undifixp  6868  dom2lem  6917  isinf  7092  unblem4  7128  unbnn2  7130  marypha1lem  7202  supiso  7239  ordiso2  7246  card2inf  7285  elirrv  7327  wemapwe  7416  trcl  7426  tz9.13  7479  rankval3b  7514  rankunb  7538  rankuni2b  7541  scott0  7572  dfac8alem  7672  carduniima  7739  alephsmo  7745  alephval3  7753  iunfictbso  7757  dfac3  7764  dfac5lem5  7770  dfac12r  7788  dfac12k  7789  kmlem4  7795  kmlem11  7802  cfsuc  7899  cofsmo  7911  cfsmolem  7912  coftr  7915  alephsing  7918  infpssrlem3  7947  fin23lem30  7984  isf32lem2  7996  isf32lem3  7997  isf34lem6  8022  fin1a2lem11  8052  fin1a2lem13  8054  fin1a2s  8056  axcc2lem  8078  domtriomlem  8084  axdc3lem2  8093  axdc4lem  8097  axcclem  8099  axdclem2  8163  iundom2g  8178  uniimadom  8182  cardmin  8202  alephval2  8210  alephreg  8220  fpwwe2lem12  8279  wunex2  8376  wuncval2  8385  tskwe2  8411  inar1  8413  tskuni  8421  gruun  8444  intgru  8452  grutsk1  8459  genpcl  8648  ltexprlem5  8680  suplem1pr  8692  supexpr  8694  supsrlem  8749  axpre-sup  8807  supmul1  9735  supmullem1  9736  supmul  9738  peano5nni  9765  uzind  10119  zindd  10129  uzwo  10297  uzwoOLD  10298  lbzbi  10322  xrsupsslem  10641  xrinfmsslem  10642  supxrun  10650  supxrpnf  10653  supxrunb1  10654  supxrunb2  10655  icoshftf1o  10775  flval3  10961  axdc4uzlem  11060  sqrlem1  11744  sqrlem6  11749  fsum0diag2  12261  alzdvds  12594  gcdcllem1  12706  maxprmfct  12808  unbenlem  12971  vdwlem6  13049  vdwlem10  13053  firest  13353  mrieqv2d  13557  iscatd  13591  setcmon  13935  setcepi  13936  isglbd  14237  isacs4lem  14287  acsfiindd  14296  acsmapd  14297  psss  14339  ghmrn  14712  ghmpreima  14720  cntz2ss  14824  lsmsubg  14981  efgsfo  15064  gsumzaddlem  15219  dmdprdd  15253  dprd2da  15293  imasrng  15418  isabvd  15601  issrngd  15642  islssd  15709  lbsextlem3  15929  lbsextlem4  15930  lidldvgen  16023  isphld  16574  tgcl  16723  distop  16749  indistopon  16754  pptbas  16761  toponmre  16846  opnnei  16873  neiuni  16875  neindisj2  16876  ordtrest2  16950  cnpnei  17009  cnindis  17036  cmpcld  17145  uncmp  17146  hauscmplem  17149  2ndc1stc  17193  1stcrest  17195  1stcelcls  17203  llyrest  17227  nllyrest  17228  cldllycmp  17237  txcls  17315  ptpjcn  17321  ptclsg  17325  dfac14lem  17327  xkoccn  17329  txlly  17346  txnlly  17347  ptrescn  17349  tx1stc  17360  xkoco1cn  17367  xkoco2cn  17368  xkococn  17370  xkoinjcn  17397  qtopeu  17423  hmeofval  17465  ordthmeolem  17508  isfild  17569  fbasrn  17595  trfil2  17598  flimclslem  17695  fclsrest  17735  fclscf  17736  flimfcls  17737  alexsubALTlem1  17757  alexsubALTlem2  17758  alexsubALTlem3  17759  alexsubALT  17761  divstgpopn  17818  isxmetd  17907  imasdsf1olem  17953  blcls  18068  prdsxmslem2  18091  dscmet  18111  nrmmetd  18113  reperflem  18339  reconnlem2  18348  xrge0tsms  18355  fsumcn  18390  cnheibor  18469  tchcph  18683  lmmbr  18700  caubl  18749  ivthlem1  18827  ovolctb  18865  ovoliunlem2  18878  ovolscalem1  18888  ovolicc2  18897  voliunlem3  18925  ismbfd  19011  mbfimaopnlem  19026  itg2le  19110  ellimc2  19243  c1liplem1  19359  plyeq0lem  19608  dgreq0  19662  aannenlem1  19724  pilem2  19844  cxpcn3lem  20103  scvxcvx  20296  musum  20447  dchrisum0flb  20675  ostth2lem2  20799  htthlem  21513  ocsh  21878  shintcli  21924  pjss2coi  22760  pjnormssi  22764  pjclem4  22795  pj3si  22803  pj3cor1i  22805  strlem3a  22848  strb  22854  hstrlem3a  22856  hstrbi  22862  spansncv2  22889  mdsl1i  22917  cvmdi  22920  mdexchi  22931  h1da  22945  mdsymlem6  23004  sumdmdii  23011  dmdbr5ati  23018  ballotlemimin  23080  rnmpt2ss  23254  supssd  23263  disjabrex  23374  disjabrexf  23375  lmdvg  23391  xrge0tsmsd  23397  pwsiga  23506  measiun  23560  cntmeas  23568  probmeasb  23648  erdszelem8  23744  cvmsss2  23820  cvmfolem  23825  eupap1  23915  rtrclreclem.min  24059  dfrtrcl2  24060  dfon2lem8  24217  dfon2lem9  24218  dfon2  24219  rdgprc  24222  trpredtr  24304  trpredmintr  24305  trpredelss  24306  dftrpred3g  24307  trpredpo  24309  trpredrec  24312  wfrlem15  24341  frr3g  24351  frrlem5b  24357  frrlem5d  24359  sltval2  24381  supaddc  24995  supadd  24996  uncum2  25213  eqfnung2  25221  repfuntw  25263  prl1  25271  prl2  25272  dstr  25274  supwlub  25377  toplat  25393  sallnei  25632  intopcoaconlem3b  25641  intopcoaconb  25643  qusp  25645  cmptdst  25671  limptlimpr2lem2  25678  lvsovso  25729  claddrvr  25751  sigadd  25752  issubrv  25775  subclrvd  25777  clsmulcv  25785  clsmulrv  25786  idsubfun  25961  cmpmor  26078  setiscat  26082  indcls2  26099  nn0prpwlem  26341  ntruni  26348  clsint2  26350  fneint  26380  reftr  26392  fnessref  26396  refssfne  26397  locfincf  26409  comppfsc  26410  neibastop1  26411  neibastop2lem  26412  sdclem2  26555  fdc  26558  seqpo  26560  prdsbnd  26620  heibor  26648  rrnequiv  26662  0idl  26753  intidl  26757  unichnidl  26759  prnc  26795  pellfundre  27069  pellfundge  27070  pellfundlb  27072  dford3lem1  27222  aomclem2  27255  frlmsslsp  27351  psgnunilem2  27521  psgnghm  27540  hashgcdeq  27620  addrcom  27783  stoweidlem35  27887  funressnfv  28096  tz6.12-afv  28141  opabex3d  28190  nbusgra  28277  nbgra0nb  28278  nbgra0edg  28281  uvtxnbgravtx  28308  fargshiftf  28381  fargshiftfva  28384  eupatrl  28385  3cyclfrgrarn  28436  bnj518  29234  bnj1137  29341  bnj1136  29343  bnj1413  29381  bnj1417  29387  bnj60  29408  lsmcv2  29841  lcvexchlem4  29849  lcvexchlem5  29850  eqlkr  29911  paddclN  30653  pclfinN  30711  ldilcnv  30926  ldilco  30927  cdleme25dN  31167  cdlemj2  31633  tendocan  31635  erng1lem  31798  erngdvlem4-rN  31810  dihord2pre  32037  dihglblem2N  32106  dochvalr  32169  hdmap14lem12  32694  hdmap14lem13  32695
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-nf 1535  df-ral 2561
  Copyright terms: Public domain W3C validator