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  1642  sp  1716  ax9  1889  cbvald  1948  ax10-16  2129  ax11eq  2132  ax11el  2133  axext4  2267  eqrdv  2281  abbi2dv  2398  abbi1dv  2399  elex22  2799  elex2  2800  spcimdv  2865  pm13.183  2908  moeq3  2942  sbc2or  2999  sbcthdv  3006  sbcimdv  3052  ssrdv  3185  ss2abdv  3246  abssdv  3247  dfnfc2  3845  intss  3883  intab  3892  dfiin2g  3936  disjss1  3999  mpteq12dva  4097  axsep  4140  el  4192  euotd  4267  reusv1  4534  reusv2lem1  4535  reusv2lem2  4536  tfisi  4649  limom  4671  ssrelrel  4787  issref  5056  asymref2  5060  iotaval  5230  iota5  5239  iotabidv  5240  funmo  5271  funco  5292  funun  5296  fununi  5316  funcnvuni  5317  nfunsn  5558  funoprabg  5943  1stconst  6207  2ndconst  6208  frxp  6225  fnwelem  6230  seqomlem2  6463  iserd  6686  findcard3  7100  frfi  7102  fiint  7133  dffi2  7176  hartogslem1  7257  wdomd  7295  ixpiunwdom  7305  sucprcreg  7313  rankval3b  7498  fseqenlem2  7652  dfac3  7748  dfac5  7755  dfac2  7757  dfac8  7761  dfac9  7762  dfacacn  7767  dfac13  7768  kmlem1  7776  kmlem6  7781  kmlem13  7788  fin23lem32  7970  axdc2lem  8074  zornn0g  8132  brdom6disj  8157  fpwwe2lem11  8262  fpwwe2lem12  8263  fpwwe2lem13  8264  hargch  8299  alephgch  8300  nqpr  8638  reclem2pr  8672  shftfn  11568  fsumiunOLD  12281  hashiunOLD  12282  ramub  13060  ramcl  13076  imasaddfnlem  13430  imasvscafn  13439  mrieqv2d  13541  mreexexd  13550  invfun  13666  mreclat  14290  letsr  14349  efgval  15026  efgi  15028  efgi2  15034  gsumval3  15191  gsumzaddlem  15203  pgpfac1lem5  15314  islbs3  15908  lbsextlem4  15914  mplsubglem  16179  mpllsslem  16180  cssmre  16593  obslbs  16630  tgcl  16707  indistopon  16738  ppttop  16744  epttop  16746  mretopd  16829  toponmre  16830  neissex  16864  lmfun  17109  2ndcdisj  17182  1stccnp  17188  kgentopon  17233  dfac14  17312  ptcnp  17316  uptx  17319  ptrescn  17333  qtoptop2  17390  filcon  17578  filssufilg  17606  rnelfmlem  17647  alexsubALTlem2  17742  prdsxmslem2  18075  mbfposr  19007  mbfinf  19020  i1fd  19036  itg1climres  19069  perfdvf  19253  taylf  19740  ex-natded9.26  20806  ex-natded9.26-2  20807  nmcexi  22606  moimd  23145  iuneq12daf  23154  iuneq12df  23155  rabbidva2  23164  abfmpeld  23218  abfmpel  23219  relexpindlem  24036  rtrclreclem.min  24044  dfrtrcl2  24045  dfpo2  24112  dfon2lem6  24144  dfon2lem8  24146  dfon2lem9  24147  dfon2  24148  mptelee  24523  eqintg  24961  inposet  25278  inttop2  25515  intopcoaconb  25540  qusp  25542  prcnt  25551  ismonc  25814  isepic  25824  bosser  26167  trer  26227  finminlem  26231  neibastop1  26308  neibastop3  26311  upixp  26403  prter1  26747  ismrcd1  26773  ttac  27129  fnwe2  27150  aomclem6  27156  dfac11  27160  dfac21  27164  hbtlem2  27328  sbeqalbi  27600  ax10ext  27606  pm13.192  27610  pm14.24  27632  itgsinexplem1  27748  funressnfv  27991  nbusgra  28143  sbcssOLD  28306  gen11  28388  trsspwALT2  28593  snssiALT  28603  sstrALT2  28611  en3lpVD  28621  sspwimp  28694  sspwimpcf  28696  sspwimpALT  28701  sspwimpALT2  28705  a9e2ndeqALT  28708  bnj145  28755  bnj1143  28822  bnj1379  28863  bnj149  28907
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