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

Theorem alrimiv 1617
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 1603 . 2  |-  ( ph  ->  A. x ph )
2 alrimiv.1 . 2  |-  ( ph  ->  ps )
31, 2alrimih 1552 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527
This theorem is referenced by:  alrimivv  1618  nfdv  1620  cbvalivw  1643  sp  1717  ax9  1891  cbvald  1953  ax10-16  2131  ax11eq  2133  ax11el  2134  axext4  2268  eqrdv  2282  abbi2dv  2399  abbi1dv  2400  elex22  2800  elex2  2801  spcimdv  2866  pm13.183  2909  moeq3  2943  sbc2or  3000  sbcthdv  3007  sbcimdv  3053  ssrdv  3186  ss2abdv  3247  abssdv  3248  dfnfc2  3846  intss  3884  intab  3893  dfiin2g  3937  disjss1  4000  mpteq12dva  4098  axsep  4141  el  4191  euotd  4266  reusv1  4533  reusv2lem1  4534  reusv2lem2  4535  tfisi  4648  limom  4670  ssrelrel  4786  issref  5055  asymref2  5059  funmo  5237  funco  5258  funun  5262  fununi  5282  funcnvuni  5283  nfunsn  5520  funoprabg  5905  1stconst  6169  2ndconst  6170  frxp  6187  fnwelem  6192  iotaval  6264  iota5  6273  iotabidv  6274  seqomlem2  6459  iserd  6682  findcard3  7096  frfi  7098  fiint  7129  dffi2  7172  hartogslem1  7253  wdomd  7291  ixpiunwdom  7301  sucprcreg  7309  rankval3b  7494  fseqenlem2  7648  dfac3  7744  dfac5  7751  dfac2  7753  dfac8  7757  dfac9  7758  dfacacn  7763  dfac13  7764  kmlem1  7772  kmlem6  7777  kmlem13  7784  fin23lem32  7966  axdc2lem  8070  zornn0g  8128  brdom6disj  8153  fpwwe2lem11  8258  fpwwe2lem12  8259  fpwwe2lem13  8260  hargch  8295  alephgch  8296  nqpr  8634  reclem2pr  8668  shftfn  11564  fsumiunOLD  12277  hashiunOLD  12278  ramub  13056  ramcl  13072  imasaddfnlem  13426  imasvscafn  13435  mrieqv2d  13537  mreexexd  13546  invfun  13662  mreclat  14286  letsr  14345  efgval  15022  efgi  15024  efgi2  15030  gsumval3  15187  gsumzaddlem  15199  pgpfac1lem5  15310  islbs3  15904  lbsextlem4  15910  mplsubglem  16175  mpllsslem  16176  cssmre  16589  obslbs  16626  tgcl  16703  indistopon  16734  ppttop  16740  epttop  16742  mretopd  16825  toponmre  16826  neissex  16860  lmfun  17105  2ndcdisj  17178  1stccnp  17184  kgentopon  17229  dfac14  17308  ptcnp  17312  uptx  17315  ptrescn  17329  qtoptop2  17386  filcon  17574  filssufilg  17602  rnelfmlem  17643  alexsubALTlem2  17738  prdsxmslem2  18071  mbfposr  19003  mbfinf  19016  i1fd  19032  itg1climres  19065  perfdvf  19249  taylf  19736  ex-natded9.26  20828  ex-natded9.26-2  20829  nmcexi  22602  relexpindlem  23443  rtrclreclem.min  23451  dfrtrcl2  23452  dfpo2  23518  dfon2lem6  23548  dfon2lem8  23550  dfon2lem9  23551  dfon2  23552  elfuns  23864  mptelee  23933  eqintg  24371  inposet  24689  inttop2  24926  intopcoaconb  24951  qusp  24953  prcnt  24962  ismonc  25225  isepic  25235  bosser  25578  trer  25638  finminlem  25642  neibastop1  25719  neibastop3  25722  upixp  25814  prter1  26158  ismrcd1  26184  ttac  26540  fnwe2  26561  aomclem6  26567  dfac11  26571  dfac21  26575  hbtlem2  26739  sbeqalbi  27011  ax10ext  27017  pm13.192  27021  pm14.24  27043  itgsinexplem1  27159  funressnfv  27382  sbcssOLD  27589  gen11  27668  trsspwALT2  27873  snssiALT  27883  sstrALT2  27891  en3lpVD  27901  sspwimp  27974  sspwimpcf  27976  sspwimpALT  27981  sspwimpALT2  27985  a9e2ndeqALT  27988  bnj145  28034  bnj1143  28101  bnj1379  28142  bnj149  28186
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603
  Copyright terms: Public domain W3C validator