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

Theorem alrimiv 1619
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 1605 . 2  |-  ( ph  ->  A. x ph )
2 alrimiv.1 . 2  |-  ( ph  ->  ps )
31, 2alrimih 1554 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1529
This theorem is referenced by:  alrimivv  1620  nfdv  1622  cbvalivw  1644  sp  1718  ax9  1891  cbvald  1950  ax10-16  2131  ax11eq  2134  ax11el  2135  axext4  2269  eqrdv  2283  abbi2dv  2400  abbi1dv  2401  elex22  2801  elex2  2802  spcimdv  2867  pm13.183  2910  moeq3  2944  sbc2or  3001  sbcthdv  3008  sbcimdv  3054  ssrdv  3187  ss2abdv  3248  abssdv  3249  dfnfc2  3847  intss  3885  intab  3894  dfiin2g  3938  disjss1  4001  mpteq12dva  4099  axsep  4142  el  4194  euotd  4269  reusv1  4536  reusv2lem1  4537  reusv2lem2  4538  tfisi  4651  limom  4673  ssrelrel  4789  issref  5058  asymref2  5062  iotaval  5232  iota5  5241  iotabidv  5242  funmo  5273  funco  5294  funun  5298  fununi  5318  funcnvuni  5319  nfunsn  5560  funoprabg  5945  1stconst  6209  2ndconst  6210  frxp  6227  fnwelem  6232  seqomlem2  6465  iserd  6688  findcard3  7102  frfi  7104  fiint  7135  dffi2  7178  hartogslem1  7259  wdomd  7297  ixpiunwdom  7307  sucprcreg  7315  rankval3b  7500  fseqenlem2  7654  dfac3  7750  dfac5  7757  dfac2  7759  dfac8  7763  dfac9  7764  dfacacn  7769  dfac13  7770  kmlem1  7778  kmlem6  7783  kmlem13  7790  fin23lem32  7972  axdc2lem  8076  zornn0g  8134  brdom6disj  8159  fpwwe2lem11  8264  fpwwe2lem12  8265  fpwwe2lem13  8266  hargch  8301  alephgch  8302  nqpr  8640  reclem2pr  8674  shftfn  11570  fsumiunOLD  12283  hashiunOLD  12284  ramub  13062  ramcl  13078  imasaddfnlem  13432  imasvscafn  13441  mrieqv2d  13543  mreexexd  13552  invfun  13668  mreclat  14292  letsr  14351  efgval  15028  efgi  15030  efgi2  15036  gsumval3  15193  gsumzaddlem  15205  pgpfac1lem5  15316  islbs3  15910  lbsextlem4  15916  mplsubglem  16181  mpllsslem  16182  cssmre  16595  obslbs  16632  tgcl  16709  indistopon  16740  ppttop  16746  epttop  16748  mretopd  16831  toponmre  16832  neissex  16866  lmfun  17111  2ndcdisj  17184  1stccnp  17190  kgentopon  17235  dfac14  17314  ptcnp  17318  uptx  17321  ptrescn  17335  qtoptop2  17392  filcon  17580  filssufilg  17608  rnelfmlem  17649  alexsubALTlem2  17744  prdsxmslem2  18077  mbfposr  19009  mbfinf  19022  i1fd  19038  itg1climres  19071  perfdvf  19255  taylf  19742  ex-natded9.26  20808  ex-natded9.26-2  20809  nmcexi  22608  moimd  23147  iuneq12daf  23156  iuneq12df  23157  rabbidva2  23166  abfmpeld  23220  abfmpel  23221  relexpindlem  24038  rtrclreclem.min  24046  dfrtrcl2  24047  dfpo2  24114  dfon2lem6  24146  dfon2lem8  24148  dfon2lem9  24149  dfon2  24150  mptelee  24525  itg2addnc  24935  eqintg  24972  inposet  25289  inttop2  25526  intopcoaconb  25551  qusp  25553  prcnt  25562  ismonc  25825  isepic  25835  bosser  26178  trer  26238  finminlem  26242  neibastop1  26319  neibastop3  26322  upixp  26414  prter1  26758  ismrcd1  26784  ttac  27140  fnwe2  27161  aomclem6  27167  dfac11  27171  dfac21  27175  hbtlem2  27339  sbeqalbi  27611  ax10ext  27617  pm13.192  27621  pm14.24  27643  itgsinexplem1  27759  funressnfv  28002  nbusgra  28154  sbcssOLD  28362  gen11  28450  trsspwALT2  28666  snssiALT  28676  sstrALT2  28684  en3lpVD  28694  sspwimp  28767  sspwimpcf  28769  sspwimpALT  28774  sspwimpALT2  28778  a9e2ndeqALT  28781  bnj145  28828  bnj1143  28895  bnj1379  28936  bnj149  28980
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605
  Copyright terms: Public domain W3C validator