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

Theorem alrimiv 1641
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
alrimiv.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
alrimiv  |-  ( ph  ->  A. x ps )
Distinct variable group:    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem alrimiv
StepHypRef Expression
1 ax-17 1626 . 2  |-  ( ph  ->  A. x ph )
2 alrimiv.1 . 2  |-  ( ph  ->  ps )
31, 2alrimih 1574 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1549
This theorem is referenced by:  alrimivv  1642  nfdv  1649  cbvalivw  1686  spOLD  1764  cbvaldOLD  1987  ax12olem1  2005  ax9OLD  2033  ax10-16  2266  ax11eq  2269  ax11el  2270  axext4  2419  eqrdv  2433  abbi2dv  2550  abbi1dv  2551  elex22  2959  elex2  2960  spcimdv  3025  pm13.183  3068  moeq3  3103  sbc2or  3161  sbcthdv  3168  sbcimdv  3214  ssrdv  3346  ss2abdv  3408  abssdv  3409  dfnfc2  4025  intss  4063  intab  4072  dfiin2g  4116  disjss1  4180  mpteq12dva  4278  axsep  4321  el  4373  euotd  4449  reusv1  4715  reusv2lem1  4716  reusv2lem2  4717  tfisi  4830  limom  4852  ssrelrel  4968  issref  5239  asymref2  5243  iotaval  5421  iota5  5430  iotabidv  5431  funmo  5462  funco  5483  funun  5487  fununi  5509  funcnvuni  5510  nfunsn  5753  funoprabg  6161  1stconst  6427  2ndconst  6428  frxp  6448  fnwelem  6453  seqomlem2  6700  iserd  6923  findcard3  7342  frfi  7344  fiint  7375  dffi2  7420  hartogslem1  7503  wdomd  7541  ixpiunwdom  7551  sucprcreg  7559  rankval3b  7744  fseqenlem2  7898  dfac3  7994  dfac5  8001  dfac2  8003  dfac8  8007  dfac9  8008  dfacacn  8013  dfac13  8014  kmlem1  8022  kmlem6  8027  kmlem13  8034  fin23lem32  8216  axdc2lem  8320  zornn0g  8377  brdom6disj  8402  fpwwe2lem11  8507  fpwwe2lem12  8508  fpwwe2lem13  8509  hargch  8544  alephgch  8545  nqpr  8883  reclem2pr  8917  shftfn  11880  fsumiunOLD  12594  hashiunOLD  12595  ramub  13373  ramcl  13389  imasaddfnlem  13745  imasvscafn  13754  mrieqv2d  13856  mreexexd  13865  invfun  13981  mreclat  14605  letsr  14664  efgval  15341  efgi  15343  efgi2  15349  gsumval3  15506  gsumzaddlem  15518  pgpfac1lem5  15629  islbs3  16219  lbsextlem4  16225  mplsubglem  16490  mpllsslem  16491  cssmre  16912  obslbs  16949  tgcl  17026  indistopon  17057  ppttop  17063  epttop  17065  mretopd  17148  toponmre  17149  neissex  17183  neiptoptop  17187  lmfun  17437  2ndcdisj  17511  1stccnp  17517  kgentopon  17562  dfac14  17642  ptcnp  17646  uptx  17649  ptrescn  17663  qtoptop2  17723  filcon  17907  filssufilg  17935  rnelfmlem  17976  alexsubALTlem2  18071  cnextfun  18087  utoptop  18256  prdsxmslem2  18551  vitalilem3  19494  mbfposr  19536  mbfinf  19549  i1fd  19565  itg1climres  19598  perfdvf  19782  taylf  20269  ex-natded9.26  21719  ex-natded9.26-2  21720  nmcexi  23521  moimd  23966  iuneq12daf  23999  iuneq12df  24000  abfmpeld  24058  abfmpel  24059  relexpindlem  25131  rtrclreclem.min  25139  dfrtrcl2  25140  dfpo2  25370  dfon2lem6  25407  dfon2lem8  25409  dfon2lem9  25410  dfon2  25411  mptelee  25826  mblfinlem2  26235  ismblfin  26237  itg2addnc  26249  trer  26310  finminlem  26312  neibastop1  26379  neibastop3  26382  upixp  26422  prter1  26719  ismrcd1  26743  ttac  27098  fnwe2  27119  aomclem6  27125  dfac11  27128  dfac21  27132  hbtlem2  27296  sbeqalbi  27568  ax10ext  27574  pm13.192  27578  pm14.24  27600  itgsinexplem1  27715  funressnfv  27959  cshwsexa  28254  sbcssOLD  28564  gen11  28654  trsspwALT2  28869  snssiALT  28877  sstrALT2  28884  en3lpVD  28894  sspwimp  28967  sspwimpcf  28969  sspwimpALT  28974  a9e2ndeqALT  28980  bnj145  29031  bnj1143  29098  bnj1379  29139  bnj149  29183  ax9NEW7  29405  cbvaldwAUX7  29452  hbaew3AUX7  29461  ax7w15lemxAUX7  29603  cbvaldOLD7  29671
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626
  Copyright terms: Public domain W3C validator