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

Theorem alrimiv 1642
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 1627 . 2  |-  ( ph  ->  A. x ph )
2 alrimiv.1 . 2  |-  ( ph  ->  ps )
31, 2alrimih 1575 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1550
This theorem is referenced by:  alrimivv  1643  nfdv  1650  cbvalivw  1687  spOLD  1765  cbvaldOLD  1988  ax12olem1  2006  ax9OLD  2034  ax10-16  2269  ax11eq  2272  ax11el  2273  axext4  2422  eqrdv  2436  abbi2dv  2553  abbi1dv  2554  elex22  2969  elex2  2970  spcimdv  3035  pm13.183  3078  moeq3  3113  sbc2or  3171  sbcthdv  3178  sbcimdv  3224  ssrdv  3356  ss2abdv  3418  abssdv  3419  dfnfc2  4035  intss  4073  intab  4082  dfiin2g  4126  disjss1  4191  mpteq12dva  4289  axsep  4332  el  4384  euotd  4460  reusv1  4726  reusv2lem1  4727  reusv2lem2  4728  tfisi  4841  limom  4863  ssrelrel  4979  issref  5250  asymref2  5254  iotaval  5432  iota5  5441  iotabidv  5442  funmo  5473  funco  5494  funun  5498  fununi  5520  funcnvuni  5521  nfunsn  5764  funoprabg  6172  1stconst  6438  2ndconst  6439  frxp  6459  fnwelem  6464  seqomlem2  6711  iserd  6934  findcard3  7353  frfi  7355  fiint  7386  dffi2  7431  hartogslem1  7514  wdomd  7552  ixpiunwdom  7562  sucprcreg  7570  rankval3b  7755  fseqenlem2  7911  dfac3  8007  dfac5  8014  dfac2  8016  dfac8  8020  dfac9  8021  dfacacn  8026  dfac13  8027  kmlem1  8035  kmlem6  8040  kmlem13  8047  fin23lem32  8229  axdc2lem  8333  zornn0g  8390  brdom6disj  8415  fpwwe2lem11  8520  fpwwe2lem12  8521  fpwwe2lem13  8522  hargch  8553  alephgch  8554  nqpr  8896  reclem2pr  8930  shftfn  11893  fsumiunOLD  12607  hashiunOLD  12608  ramub  13386  ramcl  13402  imasaddfnlem  13758  imasvscafn  13767  mrieqv2d  13869  mreexexd  13878  invfun  13994  mreclat  14618  letsr  14677  efgval  15354  efgi  15356  efgi2  15362  gsumval3  15519  gsumzaddlem  15531  pgpfac1lem5  15642  islbs3  16232  lbsextlem4  16238  mplsubglem  16503  mpllsslem  16504  cssmre  16925  obslbs  16962  tgcl  17039  indistopon  17070  ppttop  17076  epttop  17078  mretopd  17161  toponmre  17162  neissex  17196  neiptoptop  17200  lmfun  17450  2ndcdisj  17524  1stccnp  17530  kgentopon  17575  dfac14  17655  ptcnp  17659  uptx  17662  ptrescn  17676  qtoptop2  17736  filcon  17920  filssufilg  17948  rnelfmlem  17989  alexsubALTlem2  18084  cnextfun  18100  utoptop  18269  prdsxmslem2  18564  vitalilem3  19507  mbfposr  19547  mbfinf  19560  i1fd  19576  itg1climres  19609  perfdvf  19795  taylf  20282  ex-natded9.26  21732  ex-natded9.26-2  21733  nmcexi  23534  moimd  23979  iuneq12daf  24012  iuneq12df  24013  abfmpeld  24071  abfmpel  24072  relexpindlem  25144  rtrclreclem.min  25152  dfrtrcl2  25153  dfpo2  25383  dfon2lem6  25420  dfon2lem8  25422  dfon2lem9  25423  dfon2  25424  mptelee  25839  mblfinlem3  26257  ismblfin  26259  itg2addnc  26273  trer  26333  finminlem  26335  neibastop1  26402  neibastop3  26405  upixp  26445  prter1  26742  ismrcd1  26766  ttac  27121  fnwe2  27142  aomclem6  27148  dfac11  27151  dfac21  27155  hbtlem2  27319  sbeqalbi  27591  ax10ext  27597  pm13.192  27601  pm14.24  27623  itgsinexplem1  27738  funressnfv  27982  cshwsexa  28325  sbcssOLD  28701  gen11  28791  trsspwALT2  29006  snssiALT  29014  sstrALT2  29021  en3lpVD  29031  sspwimp  29104  sspwimpcf  29106  sspwimpALT  29111  a9e2ndeqALT  29117  bnj145  29168  bnj1143  29235  bnj1379  29276  bnj149  29320  ax9NEW7  29542  cbvaldwAUX7  29589  hbaew3AUX7  29598  ax7w15lemxAUX7  29740  cbvaldOLD7  29808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1556  ax-5 1567  ax-17 1627
  Copyright terms: Public domain W3C validator