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

Theorem alrimiv 1621
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 1606 . 2  |-  ( ph  ->  A. x ph )
2 alrimiv.1 . 2  |-  ( ph  ->  ps )
31, 2alrimih 1555 1  |-  ( ph  ->  A. x ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530
This theorem is referenced by:  alrimivv  1622  nfdv  1629  cbvalivw  1660  sp  1728  ax9  1902  cbvald  1961  ax10-16  2142  ax11eq  2145  ax11el  2146  axext4  2280  eqrdv  2294  abbi2dv  2411  abbi1dv  2412  elex22  2812  elex2  2813  spcimdv  2878  pm13.183  2921  moeq3  2955  sbc2or  3012  sbcthdv  3019  sbcimdv  3065  ssrdv  3198  ss2abdv  3259  abssdv  3260  dfnfc2  3861  intss  3899  intab  3908  dfiin2g  3952  disjss1  4015  mpteq12dva  4113  axsep  4156  el  4208  euotd  4283  reusv1  4550  reusv2lem1  4551  reusv2lem2  4552  tfisi  4665  limom  4687  ssrelrel  4803  issref  5072  asymref2  5076  iotaval  5246  iota5  5255  iotabidv  5256  funmo  5287  funco  5308  funun  5312  fununi  5332  funcnvuni  5333  nfunsn  5574  funoprabg  5959  1stconst  6223  2ndconst  6224  frxp  6241  fnwelem  6246  seqomlem2  6479  iserd  6702  findcard3  7116  frfi  7118  fiint  7149  dffi2  7192  hartogslem1  7273  wdomd  7311  ixpiunwdom  7321  sucprcreg  7329  rankval3b  7514  fseqenlem2  7668  dfac3  7764  dfac5  7771  dfac2  7773  dfac8  7777  dfac9  7778  dfacacn  7783  dfac13  7784  kmlem1  7792  kmlem6  7797  kmlem13  7804  fin23lem32  7986  axdc2lem  8090  zornn0g  8148  brdom6disj  8173  fpwwe2lem11  8278  fpwwe2lem12  8279  fpwwe2lem13  8280  hargch  8315  alephgch  8316  nqpr  8654  reclem2pr  8688  shftfn  11584  fsumiunOLD  12297  hashiunOLD  12298  ramub  13076  ramcl  13092  imasaddfnlem  13446  imasvscafn  13455  mrieqv2d  13557  mreexexd  13566  invfun  13682  mreclat  14306  letsr  14365  efgval  15042  efgi  15044  efgi2  15050  gsumval3  15207  gsumzaddlem  15219  pgpfac1lem5  15330  islbs3  15924  lbsextlem4  15930  mplsubglem  16195  mpllsslem  16196  cssmre  16609  obslbs  16646  tgcl  16723  indistopon  16754  ppttop  16760  epttop  16762  mretopd  16845  toponmre  16846  neissex  16880  lmfun  17125  2ndcdisj  17198  1stccnp  17204  kgentopon  17249  dfac14  17328  ptcnp  17332  uptx  17335  ptrescn  17349  qtoptop2  17406  filcon  17594  filssufilg  17622  rnelfmlem  17663  alexsubALTlem2  17758  prdsxmslem2  18091  mbfposr  19023  mbfinf  19036  i1fd  19052  itg1climres  19085  perfdvf  19269  taylf  19756  ex-natded9.26  20822  ex-natded9.26-2  20823  nmcexi  22622  moimd  23161  iuneq12daf  23170  iuneq12df  23171  rabbidva2  23180  abfmpeld  23233  abfmpel  23234  relexpindlem  24051  rtrclreclem.min  24059  dfrtrcl2  24060  dfpo2  24183  dfon2lem6  24215  dfon2lem8  24217  dfon2lem9  24218  dfon2  24219  mptelee  24595  itg2addnc  25005  eqintg  25064  inposet  25381  inttop2  25618  intopcoaconb  25643  qusp  25645  prcnt  25654  ismonc  25917  isepic  25927  bosser  26270  trer  26330  finminlem  26334  neibastop1  26411  neibastop3  26414  upixp  26506  prter1  26850  ismrcd1  26876  ttac  27232  fnwe2  27253  aomclem6  27259  dfac11  27263  dfac21  27267  hbtlem2  27431  sbeqalbi  27703  ax10ext  27709  pm13.192  27713  pm14.24  27735  itgsinexplem1  27851  funressnfv  28096  nbusgra  28277  sbcssOLD  28605  gen11  28693  trsspwALT2  28909  snssiALT  28919  sstrALT2  28927  en3lpVD  28937  sspwimp  29010  sspwimpcf  29012  sspwimpALT  29017  sspwimpALT2  29021  a9e2ndeqALT  29024  bnj145  29071  bnj1143  29138  bnj1379  29179  bnj149  29223  ax9NEW7  29445  hbaew3AUX7  29499  cbvaldOLD7  29688
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606
  Copyright terms: Public domain W3C validator