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

Theorem alrimiv 2004
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2222 and 19.21v 2017. (Contributed by NM, 21-Jun-1993.)
Hypothesis
Ref Expression
alrimiv.1 (𝜑𝜓)
Assertion
Ref Expression
alrimiv (𝜑 → ∀𝑥𝜓)
Distinct variable group:   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem alrimiv
StepHypRef Expression
1 ax-5 1988 . 2 (𝜑 → ∀𝑥𝜑)
2 alrimiv.1 . 2 (𝜑𝜓)
31, 2alrimih 1900 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1871  ax-4 1886  ax-5 1988
This theorem is referenced by:  alrimivv  2005  nexdvOLD  2014  nfdvOLD  2039  cbvalivw  2089  equvelv  2114  aevlem0  2131  aev  2134  hbaevg  2135  aev2ALT  2138  nf5dv  2174  euequ1  2613  axext4  2744  eqrdv  2758  abbi2dv  2880  elex2  3356  elex22  3357  spcimdv  3430  pm13.183  3484  moeq3  3524  sbc2or  3585  sbcthdv  3592  sbcimdv  3639  sbcimdvOLD  3640  ssrdv  3750  ss2abdv  3816  abssdv  3817  dfnfc2  4606  dfnfc2OLD  4607  intab  4659  iuneq12df  4696  dfiin2g  4705  disjss1  4778  mpteq12dva  4884  axsep  4932  el  4996  reusv1OLD  5016  reusv2lem1  5017  reusv2lem2  5018  reusv2lem2OLD  5019  euotd  5123  ssrelrel  5377  issref  5667  asymref2  5671  iotaval  6023  iota5  6032  iotabidv  6033  funmo  6065  funco  6089  funun  6093  fununfun  6095  fununi  6125  nfunsn  6387  fvn0ssdmfun  6514  f1oresrab  6559  funoprabg  6925  tfisi  7224  limom  7246  funcnvuni  7285  1stconst  7434  2ndconst  7435  frxp  7456  fnwelem  7461  seqomlem2  7716  iserd  7939  findcard3  8370  frfi  8372  fiint  8404  dffi2  8496  hartogslem1  8614  wdomd  8653  ixpiunwdom  8663  rankval3b  8864  fseqenlem2  9058  dfac3  9154  dfac5  9161  dfac2b  9163  dfac2OLD  9165  dfac8  9169  dfac9  9170  dfacacn  9175  dfac13  9176  kmlem1  9184  kmlem6  9189  kmlem13  9196  fin23lem32  9378  axdc2lem  9482  zornn0g  9539  brdom6disj  9566  fpwwe2lem11  9674  fpwwe2lem12  9675  fpwwe2lem13  9676  hargch  9707  alephgch  9708  nqpr  10048  reclem2pr  10082  cshwsexa  13790  rtrclreclem4  14020  dfrtrcl2  14021  relexpindlem  14022  shftfn  14032  ramub  15939  ramcl  15955  imasaddfnlem  16410  imasvscafn  16419  mrieqv2d  16521  mreexexd  16530  invfun  16645  joinfval  17222  meetfval  17236  mreclatBAD  17408  letsr  17448  efgval  18350  efgi  18352  efgi2  18358  gsumval3lem2  18527  gsumzaddlem  18541  pgpfac1lem5  18698  islbs3  19377  lbsextlem4  19383  mplsubglem  19656  mpllsslem  19657  cssmre  20259  obslbs  20296  tgcl  20995  indistopon  21027  ppttop  21033  epttop  21035  mretopd  21118  toponmre  21119  neissex  21153  neiptoptop  21157  lmfun  21407  2ndcdisj  21481  1stccnp  21487  kgentopon  21563  dfac14  21643  ptcnp  21647  uptx  21650  ptrescn  21664  qtoptop2  21724  filconn  21908  filssufilg  21936  rnelfmlem  21977  alexsubALTlem2  22073  cnextfun  22089  utoptop  22259  prdsxmslem2  22555  vitalilem3  23598  mbfposr  23638  mbfinf  23651  i1fd  23667  itg1climres  23700  perfdvf  23886  taylf  24334  mptelee  25995  upgr1eopALT  26232  upgrspanop  26409  umgrspanop  26410  usgrspanop  26411  cplgrop  26564  umgr2v2enb1  26653  iswspthsnon  26982  clwwlknon1loop  27267  wlkl0  27549  ex-natded9.26  27608  ex-natded9.26-2  27609  aevdemo  27649  nmcexi  29215  moimd  29656  rabeqsnd  29670  iuneq12daf  29701  abfmpeld  29784  abfmpel  29785  fpwrelmap  29838  rngurd  30118  bnj1143  31189  bnj1379  31229  bnj149  31273  mclsssvlem  31787  ssmclslem  31790  mclsax  31794  mclsind  31795  dfpo2  31973  dfon2lem6  32019  dfon2lem8  32021  dfon2lem9  32022  dfon2  32023  trer  32637  finminlem  32639  neibastop1  32681  neibastop3  32684  unblimceq0  32825  unbdqndv1  32826  knoppndv  32852  bj-alsb  32953  bj-ssbequ1  32972  bj-ssbid1ALT  32976  bj-eqs  32991  bj-elequ2g  32994  bj-sb  33005  bj-abbi2dv  33108  bj-axsep  33121  bj-el  33124  bj-spcimdv  33206  bj-spcimdvv  33207  bj-csbprc  33226  bj-cleq  33273  bj-ismooredr  33388  exellimddv  33522  wl-cbv3vv  33638  fin2so  33727  poimirlem17  33757  mblfinlem3  33779  ismblfin  33781  itg2addnc  33795  upixp  33855  mpt2bi123f  34302  mptbi12f  34306  trcoss  34573  prter1  34686  axc11n-16  34745  ax12eq  34748  ax12el  34749  ismrcd1  37781  ttac  38123  fnwe2  38143  aomclem6  38149  dfac11  38152  dfac21  38156  hbtlem2  38214  cllem0  38391  clss2lem  38438  mptrcllem  38440  iunrelexpmin1  38520  iunrelexpmin2  38524  iunrelexpuztr  38531  dftrcl3  38532  brtrclfv2  38539  dfrtrcl3  38545  psshepw  38602  frege91  38768  frege97  38774  frege109  38786  frege130  38807  neik0pk1imk0  38865  sbeqalbi  39121  axc11next  39127  pm13.192  39131  pm14.24  39153  gen11  39361  trsspwALT2  39566  snssiALT  39580  sstrALT2  39587  en3lpVD  39597  sspwimp  39671  sspwimpcf  39673  sspwimpALT  39678  ax6e2ndeqALT  39684  rnmptpr  39875  ssmapsn  39925  infnsuprnmpt  39982  uzinico  40308  icccncfext  40621  itgsinexplem1  40690  sge0resplit  41144  hoidmvlelem1  41333  hspdifhsp  41354  smflimsuplem7  41556  funressnfv  41732  iccpartdisj  41901  zrinitorngc  42528  zrtermorngc  42529  zrtermoringc  42598  setrec2fun  42967  elsetrecslem  42973  setrecsss  42975  setrecsres  42976  0setrec  42978
  Copyright terms: Public domain W3C validator