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

Theorem alrimiv 1638
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 1623 . 2  |-  ( ph  ->  A. x ph )
2 alrimiv.1 . 2  |-  ( ph  ->  ps )
31, 2alrimih 1571 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1546
This theorem is referenced by:  alrimivv  1639  nfdv  1646  cbvalivw  1681  spOLD  1756  ax12olem1  1962  ax9OLD  1991  cbvald  2043  ax10-16  2225  ax11eq  2228  ax11el  2229  axext4  2372  eqrdv  2386  abbi2dv  2503  abbi1dv  2504  elex22  2911  elex2  2912  spcimdv  2977  pm13.183  3020  moeq3  3055  sbc2or  3113  sbcthdv  3120  sbcimdv  3166  ssrdv  3298  ss2abdv  3360  abssdv  3361  dfnfc2  3976  intss  4014  intab  4023  dfiin2g  4067  disjss1  4130  mpteq12dva  4228  axsep  4271  el  4323  euotd  4399  reusv1  4664  reusv2lem1  4665  reusv2lem2  4666  tfisi  4779  limom  4801  ssrelrel  4917  issref  5188  asymref2  5192  iotaval  5370  iota5  5379  iotabidv  5380  funmo  5411  funco  5432  funun  5436  fununi  5458  funcnvuni  5459  nfunsn  5702  funoprabg  6109  1stconst  6375  2ndconst  6376  frxp  6393  fnwelem  6398  seqomlem2  6645  iserd  6868  findcard3  7287  frfi  7289  fiint  7320  dffi2  7364  hartogslem1  7445  wdomd  7483  ixpiunwdom  7493  sucprcreg  7501  rankval3b  7686  fseqenlem2  7840  dfac3  7936  dfac5  7943  dfac2  7945  dfac8  7949  dfac9  7950  dfacacn  7955  dfac13  7956  kmlem1  7964  kmlem6  7969  kmlem13  7976  fin23lem32  8158  axdc2lem  8262  zornn0g  8319  brdom6disj  8344  fpwwe2lem11  8449  fpwwe2lem12  8450  fpwwe2lem13  8451  hargch  8486  alephgch  8487  nqpr  8825  reclem2pr  8859  shftfn  11816  fsumiunOLD  12530  hashiunOLD  12531  ramub  13309  ramcl  13325  imasaddfnlem  13681  imasvscafn  13690  mrieqv2d  13792  mreexexd  13801  invfun  13917  mreclat  14541  letsr  14600  efgval  15277  efgi  15279  efgi2  15285  gsumval3  15442  gsumzaddlem  15454  pgpfac1lem5  15565  islbs3  16155  lbsextlem4  16161  mplsubglem  16426  mpllsslem  16427  cssmre  16844  obslbs  16881  tgcl  16958  indistopon  16989  ppttop  16995  epttop  16997  mretopd  17080  toponmre  17081  neissex  17115  neiptoptop  17119  lmfun  17368  2ndcdisj  17441  1stccnp  17447  kgentopon  17492  dfac14  17572  ptcnp  17576  uptx  17579  ptrescn  17593  qtoptop2  17653  filcon  17837  filssufilg  17865  rnelfmlem  17906  alexsubALTlem2  18001  cnextfun  18017  utoptop  18186  prdsxmslem2  18450  vitalilem3  19370  mbfposr  19412  mbfinf  19425  i1fd  19441  itg1climres  19474  perfdvf  19658  taylf  20145  nbusgra  21307  ex-natded9.26  21576  ex-natded9.26-2  21577  nmcexi  23378  moimd  23819  iuneq12daf  23852  iuneq12df  23853  abfmpeld  23909  abfmpel  23910  relexpindlem  24919  rtrclreclem.min  24927  dfrtrcl2  24928  dfpo2  25137  dfon2lem6  25169  dfon2lem8  25171  dfon2lem9  25172  dfon2  25173  mptelee  25549  itg2addnc  25960  trer  26011  finminlem  26013  neibastop1  26080  neibastop3  26083  upixp  26123  prter1  26420  ismrcd1  26444  ttac  26799  fnwe2  26820  aomclem6  26826  dfac11  26830  dfac21  26834  hbtlem2  26998  sbeqalbi  27270  ax10ext  27276  pm13.192  27280  pm14.24  27302  itgsinexplem1  27417  funressnfv  27662  sbcssOLD  27971  gen11  28059  trsspwALT2  28274  snssiALT  28282  sstrALT2  28289  en3lpVD  28299  sspwimp  28372  sspwimpcf  28374  sspwimpALT  28379  a9e2ndeqALT  28386  bnj145  28433  bnj1143  28500  bnj1379  28541  bnj149  28585  ax9NEW7  28807  hbaew3AUX7  28861  cbvaldOLD7  29051
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623
  Copyright terms: Public domain W3C validator