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  4190  mpteq12dva  4288  axsep  4331  el  4383  euotd  4459  reusv1  4725  reusv2lem1  4726  reusv2lem2  4727  tfisi  4840  limom  4862  ssrelrel  4978  issref  5249  asymref2  5253  iotaval  5431  iota5  5440  iotabidv  5441  funmo  5472  funco  5493  funun  5497  fununi  5519  funcnvuni  5520  nfunsn  5763  funoprabg  6171  1stconst  6437  2ndconst  6438  frxp  6458  fnwelem  6463  seqomlem2  6710  iserd  6933  findcard3  7352  frfi  7354  fiint  7385  dffi2  7430  hartogslem1  7513  wdomd  7551  ixpiunwdom  7561  sucprcreg  7569  rankval3b  7754  fseqenlem2  7908  dfac3  8004  dfac5  8011  dfac2  8013  dfac8  8017  dfac9  8018  dfacacn  8023  dfac13  8024  kmlem1  8032  kmlem6  8037  kmlem13  8044  fin23lem32  8226  axdc2lem  8330  zornn0g  8387  brdom6disj  8412  fpwwe2lem11  8517  fpwwe2lem12  8518  fpwwe2lem13  8519  hargch  8554  alephgch  8555  nqpr  8893  reclem2pr  8927  shftfn  11890  fsumiunOLD  12604  hashiunOLD  12605  ramub  13383  ramcl  13399  imasaddfnlem  13755  imasvscafn  13764  mrieqv2d  13866  mreexexd  13875  invfun  13991  mreclat  14615  letsr  14674  efgval  15351  efgi  15353  efgi2  15359  gsumval3  15516  gsumzaddlem  15528  pgpfac1lem5  15639  islbs3  16229  lbsextlem4  16235  mplsubglem  16500  mpllsslem  16501  cssmre  16922  obslbs  16959  tgcl  17036  indistopon  17067  ppttop  17073  epttop  17075  mretopd  17158  toponmre  17159  neissex  17193  neiptoptop  17197  lmfun  17447  2ndcdisj  17521  1stccnp  17527  kgentopon  17572  dfac14  17652  ptcnp  17656  uptx  17659  ptrescn  17673  qtoptop2  17733  filcon  17917  filssufilg  17945  rnelfmlem  17986  alexsubALTlem2  18081  cnextfun  18097  utoptop  18266  prdsxmslem2  18561  vitalilem3  19504  mbfposr  19546  mbfinf  19559  i1fd  19575  itg1climres  19608  perfdvf  19792  taylf  20279  ex-natded9.26  21729  ex-natded9.26-2  21730  nmcexi  23531  moimd  23976  iuneq12daf  24009  iuneq12df  24010  abfmpeld  24068  abfmpel  24069  relexpindlem  25141  rtrclreclem.min  25149  dfrtrcl2  25150  dfpo2  25380  dfon2lem6  25417  dfon2lem8  25419  dfon2lem9  25420  dfon2  25421  mptelee  25836  mblfinlem3  26247  ismblfin  26249  itg2addnc  26261  trer  26321  finminlem  26323  neibastop1  26390  neibastop3  26393  upixp  26433  prter1  26730  ismrcd1  26754  ttac  27109  fnwe2  27130  aomclem6  27136  dfac11  27139  dfac21  27143  hbtlem2  27307  sbeqalbi  27579  ax10ext  27585  pm13.192  27589  pm14.24  27611  itgsinexplem1  27726  funressnfv  27970  cshwsexa  28313  sbcssOLD  28689  gen11  28779  trsspwALT2  28994  snssiALT  29002  sstrALT2  29009  en3lpVD  29019  sspwimp  29092  sspwimpcf  29094  sspwimpALT  29099  a9e2ndeqALT  29105  bnj145  29156  bnj1143  29223  bnj1379  29264  bnj149  29308  ax9NEW7  29530  cbvaldwAUX7  29577  hbaew3AUX7  29586  ax7w15lemxAUX7  29728  cbvaldOLD7  29796
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627
  Copyright terms: Public domain W3C validator