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

Theorem ralrimiv 2780
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 2779 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   A.wral 2697
This theorem is referenced by:  ralrimiva  2781  ralrimivw  2782  ralrimivv  2789  r19.27av  2836  rr19.3v  3069  rabssdv  3415  rzal  3721  trin  4304  class2seteq  4360  onmindif  4663  ralxfrALT  4734  ssorduni  4758  onminex  4779  onmindif2  4784  suceloni  4785  limuni3  4824  issref  5239  fnpr  5942  fnprOLD  5943  frxp  6448  poxp  6450  onfununi  6595  onnseq  6598  tfrlem12  6642  tz7.48-2  6691  oaass  6796  omass  6815  oelim2  6830  oelimcl  6835  oaabs2  6880  omabs  6882  undifixp  7090  dom2lem  7139  isinf  7314  unblem4  7354  unbnn2  7356  marypha1lem  7430  supiso  7469  ordiso2  7476  card2inf  7515  elirrv  7557  wemapwe  7646  trcl  7656  tz9.13  7709  rankval3b  7744  rankunb  7768  rankuni2b  7771  scott0  7802  dfac8alem  7902  carduniima  7969  alephsmo  7975  alephval3  7983  iunfictbso  7987  dfac3  7994  dfac5lem5  8000  dfac12r  8018  dfac12k  8019  kmlem4  8025  kmlem11  8032  cfsuc  8129  cofsmo  8141  cfsmolem  8142  coftr  8145  alephsing  8148  infpssrlem3  8177  fin23lem30  8214  isf32lem2  8226  isf32lem3  8227  isf34lem6  8252  fin1a2lem11  8282  fin1a2lem13  8284  fin1a2s  8286  axcc2lem  8308  domtriomlem  8314  axdc3lem2  8323  axdc4lem  8327  axcclem  8329  axdclem2  8392  iundom2g  8407  uniimadom  8411  cardmin  8431  alephval2  8439  alephreg  8449  fpwwe2lem12  8508  wunex2  8605  wuncval2  8614  tskwe2  8640  inar1  8642  tskuni  8650  gruun  8673  intgru  8681  grutsk1  8688  genpcl  8877  ltexprlem5  8909  suplem1pr  8921  supexpr  8923  supsrlem  8978  axpre-sup  9036  supmul1  9965  supmullem1  9966  supmul  9968  peano5nni  9995  uzind  10353  zindd  10363  uzwo  10531  uzwoOLD  10532  lbzbi  10556  xrsupsslem  10877  xrinfmsslem  10878  supxrun  10886  supxrpnf  10889  supxrunb1  10890  supxrunb2  10891  icoshftf1o  11012  flval3  11214  axdc4uzlem  11313  sqrlem1  12040  sqrlem6  12045  fsum0diag2  12558  alzdvds  12891  gcdcllem1  13003  maxprmfct  13105  unbenlem  13268  vdwlem6  13346  vdwlem10  13350  firest  13652  mrieqv2d  13856  iscatd  13890  setcmon  14234  setcepi  14235  isglbd  14536  isacs4lem  14586  acsfiindd  14595  acsmapd  14596  psss  14638  ghmrn  15011  ghmpreima  15019  cntz2ss  15123  lsmsubg  15280  efgsfo  15363  gsumzaddlem  15518  dmdprdd  15552  dprd2da  15592  imasrng  15717  isabvd  15900  issrngd  15941  islssd  16004  lbsextlem3  16224  lbsextlem4  16225  lidldvgen  16318  isphld  16877  tgcl  17026  distop  17052  indistopon  17057  pptbas  17064  toponmre  17149  opnnei  17176  neiuni  17178  neindisj2  17179  ordtrest2  17260  cnpnei  17320  cnindis  17348  cmpcld  17457  uncmp  17458  hauscmplem  17461  2ndc1stc  17506  1stcrest  17508  1stcelcls  17516  llyrest  17540  nllyrest  17541  cldllycmp  17550  txcls  17628  ptpjcn  17635  ptclsg  17639  dfac14lem  17641  xkoccn  17643  txlly  17660  txnlly  17661  ptrescn  17663  tx1stc  17674  xkoco1cn  17681  xkoco2cn  17682  xkococn  17684  xkoinjcn  17711  qtopeu  17740  hmeofval  17782  ordthmeolem  17825  isfild  17882  fbasrn  17908  trfil2  17911  flimclslem  18008  fclsrest  18048  fclscf  18049  flimfcls  18050  alexsubALTlem1  18070  alexsubALTlem2  18071  alexsubALTlem3  18072  alexsubALT  18074  divstgpopn  18141  isxmetd  18348  imasdsf1olem  18395  blcls  18528  prdsxmslem2  18551  metustfbasOLD  18587  metustfbas  18588  dscmet  18612  nrmmetd  18614  reperflem  18841  reconnlem2  18850  xrge0tsms  18857  fsumcn  18892  cnheibor  18972  tchcph  19186  lmmbr  19203  caubl  19252  ivthlem1  19340  ovolctb  19378  ovoliunlem2  19391  ovolscalem1  19401  ovolicc2  19410  voliunlem3  19438  ismbfd  19524  mbfimaopnlem  19539  itg2le  19623  ellimc2  19756  c1liplem1  19872  plyeq0lem  20121  dgreq0  20175  aannenlem1  20237  pilem2  20360  cxpcn3lem  20623  scvxcvx  20816  musum  20968  dchrisum0flb  21196  ostth2lem2  21320  usgrares1  21416  nbusgra  21432  nbgra0nb  21433  nbgra0edg  21436  cusgrafilem2  21481  usgrasscusgra  21484  uvtxnbgravtx  21496  fargshiftf  21615  fargshiftfva  21618  eupatrl  21682  eupap1  21690  htthlem  22412  ocsh  22777  shintcli  22823  pjss2coi  23659  pjnormssi  23663  pjclem4  23694  pj3si  23702  pj3cor1i  23704  strlem3a  23747  strb  23753  hstrlem3a  23755  hstrbi  23761  spansncv2  23788  mdsl1i  23816  cvmdi  23819  mdexchi  23830  h1da  23844  mdsymlem6  23903  sumdmdii  23910  dmdbr5ati  23917  isoun  24081  supssd  24090  xrge0tsmsd  24215  pwsiga  24505  measiun  24564  dya2iocuni  24625  erdszelem8  24876  cvmsss2  24953  cvmfolem  24958  rtrclreclem.min  25139  dfrtrcl2  25140  dfon2lem8  25409  dfon2lem9  25410  dfon2  25411  rdgprc  25414  trpredtr  25500  trpredmintr  25501  trpredelss  25502  dftrpred3g  25503  trpredpo  25505  trpredrec  25508  wfrlem15  25544  frr3g  25573  frrlem5b  25579  frrlem5d  25581  sltval2  25603  supaddc  26228  supadd  26229  mblfinlem  26234  nn0prpwlem  26306  ntruni  26311  clsint2  26313  fneint  26338  reftr  26350  fnessref  26354  refssfne  26355  locfincf  26367  comppfsc  26368  neibastop1  26369  neibastop2lem  26370  sdclem2  26427  fdc  26430  seqpo  26432  prdsbnd  26483  heibor  26511  rrnequiv  26525  0idl  26616  intidl  26620  unichnidl  26622  prnc  26658  pellfundre  26925  pellfundge  26926  pellfundlb  26928  dford3lem1  27078  aomclem2  27111  frlmsslsp  27206  psgnunilem2  27376  psgnghm  27395  hashgcdeq  27475  addrcom  27637  funressnfv  27949  tz6.12-afv  27994  otiunsndisj  28046  cshweqrep  28227  3cyclfrgrarn  28330  iunconlem2  28974  bnj518  29184  bnj1137  29291  bnj1136  29293  bnj1413  29331  bnj1417  29337  bnj60  29358  lsmcv2  29754  lcvexchlem4  29762  lcvexchlem5  29763  eqlkr  29824  paddclN  30566  pclfinN  30624  ldilcnv  30839  ldilco  30840  cdleme25dN  31080  cdlemj2  31546  tendocan  31548  erng1lem  31711  erngdvlem4-rN  31723  dihord2pre  31950  dihglblem2N  32019  dochvalr  32082  hdmap14lem12  32607  hdmap14lem13  32608
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554  df-ral 2702
  Copyright terms: Public domain W3C validator