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  1682  spOLD  1760  ax12olem1  1972  ax9OLD  1999  cbvald  2058  ax10-16  2240  ax11eq  2243  ax11el  2244  axext4  2388  eqrdv  2402  abbi2dv  2519  abbi1dv  2520  elex22  2927  elex2  2928  spcimdv  2993  pm13.183  3036  moeq3  3071  sbc2or  3129  sbcthdv  3136  sbcimdv  3182  ssrdv  3314  ss2abdv  3376  abssdv  3377  dfnfc2  3993  intss  4031  intab  4040  dfiin2g  4084  disjss1  4148  mpteq12dva  4246  axsep  4289  el  4341  euotd  4417  reusv1  4682  reusv2lem1  4683  reusv2lem2  4684  tfisi  4797  limom  4819  ssrelrel  4935  issref  5206  asymref2  5210  iotaval  5388  iota5  5397  iotabidv  5398  funmo  5429  funco  5450  funun  5454  fununi  5476  funcnvuni  5477  nfunsn  5720  funoprabg  6128  1stconst  6394  2ndconst  6395  frxp  6415  fnwelem  6420  seqomlem2  6667  iserd  6890  findcard3  7309  frfi  7311  fiint  7342  dffi2  7386  hartogslem1  7467  wdomd  7505  ixpiunwdom  7515  sucprcreg  7523  rankval3b  7708  fseqenlem2  7862  dfac3  7958  dfac5  7965  dfac2  7967  dfac8  7971  dfac9  7972  dfacacn  7977  dfac13  7978  kmlem1  7986  kmlem6  7991  kmlem13  7998  fin23lem32  8180  axdc2lem  8284  zornn0g  8341  brdom6disj  8366  fpwwe2lem11  8471  fpwwe2lem12  8472  fpwwe2lem13  8473  hargch  8508  alephgch  8509  nqpr  8847  reclem2pr  8881  shftfn  11843  fsumiunOLD  12557  hashiunOLD  12558  ramub  13336  ramcl  13352  imasaddfnlem  13708  imasvscafn  13717  mrieqv2d  13819  mreexexd  13828  invfun  13944  mreclat  14568  letsr  14627  efgval  15304  efgi  15306  efgi2  15312  gsumval3  15469  gsumzaddlem  15481  pgpfac1lem5  15592  islbs3  16182  lbsextlem4  16188  mplsubglem  16453  mpllsslem  16454  cssmre  16875  obslbs  16912  tgcl  16989  indistopon  17020  ppttop  17026  epttop  17028  mretopd  17111  toponmre  17112  neissex  17146  neiptoptop  17150  lmfun  17399  2ndcdisj  17472  1stccnp  17478  kgentopon  17523  dfac14  17603  ptcnp  17607  uptx  17610  ptrescn  17624  qtoptop2  17684  filcon  17868  filssufilg  17896  rnelfmlem  17937  alexsubALTlem2  18032  cnextfun  18048  utoptop  18217  prdsxmslem2  18512  vitalilem3  19455  mbfposr  19497  mbfinf  19510  i1fd  19526  itg1climres  19559  perfdvf  19743  taylf  20230  ex-natded9.26  21680  ex-natded9.26-2  21681  nmcexi  23482  moimd  23927  iuneq12daf  23960  iuneq12df  23961  abfmpeld  24019  abfmpel  24020  relexpindlem  25092  rtrclreclem.min  25100  dfrtrcl2  25101  dfpo2  25326  dfon2lem6  25358  dfon2lem8  25360  dfon2lem9  25361  dfon2  25362  mptelee  25738  mblfinlem2  26144  ismblfin  26146  itg2addnc  26158  trer  26209  finminlem  26211  neibastop1  26278  neibastop3  26281  upixp  26321  prter1  26618  ismrcd1  26642  ttac  26997  fnwe2  27018  aomclem6  27024  dfac11  27028  dfac21  27032  hbtlem2  27196  sbeqalbi  27468  ax10ext  27474  pm13.192  27478  pm14.24  27500  itgsinexplem1  27615  funressnfv  27859  sbcssOLD  28338  gen11  28426  trsspwALT2  28641  snssiALT  28649  sstrALT2  28656  en3lpVD  28666  sspwimp  28739  sspwimpcf  28741  sspwimpALT  28746  a9e2ndeqALT  28753  bnj145  28800  bnj1143  28867  bnj1379  28908  bnj149  28952  ax9NEW7  29174  hbaew3AUX7  29228  cbvaldOLD7  29418
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