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

Theorem alrimiv 1636
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 1621 . 2  |-  ( ph  ->  A. x ph )
2 alrimiv.1 . 2  |-  ( ph  ->  ps )
31, 2alrimih 1570 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1545
This theorem is referenced by:  alrimivv  1637  nfdv  1644  cbvalivw  1679  spOLD  1754  ax9  1962  cbvald  2021  ax10-16  2203  ax11eq  2206  ax11el  2207  axext4  2350  eqrdv  2364  abbi2dv  2481  abbi1dv  2482  elex22  2884  elex2  2885  spcimdv  2950  pm13.183  2993  moeq3  3028  sbc2or  3085  sbcthdv  3092  sbcimdv  3138  ssrdv  3271  ss2abdv  3332  abssdv  3333  dfnfc2  3947  intss  3985  intab  3994  dfiin2g  4038  disjss1  4101  mpteq12dva  4199  axsep  4242  el  4294  euotd  4370  reusv1  4637  reusv2lem1  4638  reusv2lem2  4639  tfisi  4752  limom  4774  ssrelrel  4890  issref  5159  asymref2  5163  iotaval  5333  iota5  5342  iotabidv  5343  funmo  5374  funco  5395  funun  5399  fununi  5421  funcnvuni  5422  nfunsn  5665  funoprabg  6069  1stconst  6335  2ndconst  6336  frxp  6353  fnwelem  6358  seqomlem2  6605  iserd  6828  findcard3  7247  frfi  7249  fiint  7280  dffi2  7323  hartogslem1  7404  wdomd  7442  ixpiunwdom  7452  sucprcreg  7460  rankval3b  7645  fseqenlem2  7799  dfac3  7895  dfac5  7902  dfac2  7904  dfac8  7908  dfac9  7909  dfacacn  7914  dfac13  7915  kmlem1  7923  kmlem6  7928  kmlem13  7935  fin23lem32  8117  axdc2lem  8221  zornn0g  8279  brdom6disj  8304  fpwwe2lem11  8409  fpwwe2lem12  8410  fpwwe2lem13  8411  hargch  8446  alephgch  8447  nqpr  8785  reclem2pr  8819  shftfn  11775  fsumiunOLD  12489  hashiunOLD  12490  ramub  13268  ramcl  13284  imasaddfnlem  13640  imasvscafn  13649  mrieqv2d  13751  mreexexd  13760  invfun  13876  mreclat  14500  letsr  14559  efgval  15236  efgi  15238  efgi2  15244  gsumval3  15401  gsumzaddlem  15413  pgpfac1lem5  15524  islbs3  16118  lbsextlem4  16124  mplsubglem  16389  mpllsslem  16390  cssmre  16810  obslbs  16847  tgcl  16924  indistopon  16955  ppttop  16961  epttop  16963  mretopd  17046  toponmre  17047  neissex  17081  lmfun  17326  2ndcdisj  17399  1stccnp  17405  kgentopon  17450  dfac14  17529  ptcnp  17533  uptx  17536  ptrescn  17550  qtoptop2  17607  filcon  17791  filssufilg  17819  rnelfmlem  17860  alexsubALTlem2  17955  prdsxmslem2  18288  mbfposr  19222  mbfinf  19235  i1fd  19251  itg1climres  19284  perfdvf  19468  taylf  19955  nbusgra  21110  cusgrarn  21138  ex-natded9.26  21238  ex-natded9.26-2  21239  nmcexi  23040  moimd  23489  rabbidva2  23502  iuneq12daf  23526  iuneq12df  23527  abfmpeld  23589  abfmpel  23590  neiptoptop  23764  cnextfun  23821  ustfilxp  23838  utoptop  23858  relexpindlem  24708  rtrclreclem.min  24716  dfrtrcl2  24717  dfpo2  24938  dfon2lem6  24970  dfon2lem8  24972  dfon2lem9  24973  dfon2  24974  mptelee  25350  itg2addnc  25762  trer  25819  finminlem  25823  neibastop1  25900  neibastop3  25903  upixp  25995  prter1  26338  ismrcd1  26364  ttac  26720  fnwe2  26741  aomclem6  26747  dfac11  26751  dfac21  26755  hbtlem2  26919  sbeqalbi  27191  ax10ext  27197  pm13.192  27201  pm14.24  27223  itgsinexplem1  27339  funressnfv  27584  sbcssOLD  28041  gen11  28129  trsspwALT2  28345  snssiALT  28355  sstrALT2  28363  en3lpVD  28373  sspwimp  28446  sspwimpcf  28448  sspwimpALT  28453  sspwimpALT2  28457  a9e2ndeqALT  28460  bnj145  28507  bnj1143  28574  bnj1379  28615  bnj149  28659  ax9NEW7  28881  hbaew3AUX7  28935  cbvaldOLD7  29125
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621
  Copyright terms: Public domain W3C validator