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

Theorem alrimiv 2018
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2243 and 19.21v 2031. (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 2001 . 2 (𝜑 → ∀𝑥𝜑)
2 alrimiv.1 . 2 (𝜑𝜓)
31, 2alrimih 1908 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem is referenced by:  alrimivv  2019  nexdvOLD  2028  nfdvOLD  2054  cbvalivw  2104  equvelvOLD  2131  aevlem0  2149  aev  2152  hbaevg  2153  aev2ALT  2156  nf5dvOLD  2194  cbv3v2  2348  nexmo  2640  eu6  2645  euequ  2650  moimd  2695  axext4  2799  eqrdv  2815  abbi2dv  2937  elex2  3421  elex22  3422  spcimdv  3494  pm13.183  3550  moeq3  3592  sbc2or  3653  sbcthdv  3660  sbcimdv  3706  ssrdv  3815  ss2abdv  3883  abssdv  3884  rabsn  4458  dfnfc2  4661  intab  4710  iuneq12df  4747  dfiin2g  4756  mpteq12dva  4937  axsep  4987  el  5052  reusv2lem1  5080  reusv2lem2  5081  euotd  5181  ssrelrel  5435  idrefOLD  5733  asymref2  5737  iotaval  6084  iota5  6093  iotabidv  6094  funmo  6126  funco  6150  funun  6155  fununfun  6157  fununi  6184  nfunsn  6454  fvn0ssdmfun  6581  f1oresrab  6626  funoprabg  6998  tfisi  7297  limom  7319  funcnvuni  7358  1stconst  7508  2ndconst  7509  frxp  7530  fnwelem  7535  seqomlem2  7791  iserd  8014  findcard3  8451  frfi  8453  fiint  8485  dffi2  8577  hartogslem1  8695  wdomd  8734  ixpiunwdom  8744  rankval3b  8945  fseqenlem2  9140  dfac3  9236  dfac5  9243  dfac2b  9245  dfac2OLD  9247  dfac8  9251  dfac9  9252  dfacacn  9257  dfac13  9258  kmlem1  9266  kmlem6  9271  kmlem13  9278  fin23lem32  9460  axdc2lem  9564  zornn0g  9621  fpwwe2lem11  9756  fpwwe2lem12  9757  fpwwe2lem13  9758  hargch  9789  alephgch  9790  nqpr  10130  reclem2pr  10164  cshwsexa  13813  rtrclreclem4  14043  dfrtrcl2  14044  relexpindlem  14045  shftfn  14055  ramub  15953  ramcl  15969  imasaddfnlem  16412  imasvscafn  16421  mrieqv2d  16523  mreexexd  16532  invfun  16647  joinfval  17225  meetfval  17239  mreclatBAD  17411  letsr  17451  efgval  18350  efgi  18352  efgi2  18358  gsumval3lem2  18527  gsumzaddlem  18541  pgpfac1lem5  18699  islbs3  19383  lbsextlem4  19389  mplsubglem  19662  mpllsslem  19663  cssmre  20267  obslbs  20304  tgcl  21007  indistopon  21039  ppttop  21045  epttop  21047  mretopd  21130  toponmre  21131  neissex  21165  neiptoptop  21169  lmfun  21419  2ndcdisj  21493  1stccnp  21499  kgentopon  21575  dfac14  21655  ptcnp  21659  uptx  21662  ptrescn  21676  qtoptop2  21736  filconn  21920  filssufilg  21948  rnelfmlem  21989  alexsubALTlem2  22085  cnextfun  22101  utoptop  22271  prdsxmslem2  22567  vitalilem3  23613  mbfposr  23655  mbfinf  23668  i1fd  23684  itg1climres  23717  perfdvf  23903  taylf  24351  mptelee  26011  upgr1eopALT  26248  upgrspanop  26427  umgrspanop  26428  usgrspanop  26429  cplgrop  26583  umgr2v2enb1  26672  iswspthsnon  27001  clwwlknon1loop  27288  wlkl0  27569  ex-natded9.26  27629  ex-natded9.26-2  27630  aevdemo  27670  nmcexi  29235  rabeqsnd  29689  iuneq12daf  29720  abfmpeld  29803  abfmpel  29804  fpwrelmap  29857  rngurd  30135  bnj1143  31205  bnj1379  31245  bnj149  31289  mclsssvlem  31803  ssmclslem  31806  mclsax  31810  mclsind  31811  dfpo2  31988  dfon2lem6  32034  dfon2lem8  32036  dfon2lem9  32037  dfon2  32038  trer  32652  finminlem  32654  neibastop1  32696  neibastop3  32699  unblimceq0  32836  unbdqndv1  32837  knoppndv  32863  bj-alsb  32962  bj-ssbequ1  32980  bj-ssbid1ALT  32984  bj-eqs  32999  bj-elequ2g  33002  bj-sb  33013  bj-abbi2dv  33112  bj-axsep  33125  bj-el  33128  bj-spcimdv  33210  bj-spcimdvv  33211  bj-csbprc  33230  bj-cleq  33277  bj-ismooredr  33393  exellimddv  33527  fin2so  33727  poimirlem17  33757  mblfinlem3  33779  ismblfin  33781  itg2addnc  33794  upixp  33854  mpt2bi123f  34299  mptbi12f  34303  trcoss  34563  prter1  34676  axc11n-16  34735  ax12eq  34738  ax12el  34739  ismrcd1  37780  ttac  38121  fnwe2  38141  aomclem6  38147  dfac11  38150  dfac21  38154  hbtlem2  38212  cllem0  38388  clss2lem  38435  mptrcllem  38437  iunrelexpmin1  38517  iunrelexpmin2  38521  iunrelexpuztr  38528  dftrcl3  38529  brtrclfv2  38536  dfrtrcl3  38542  psshepw  38599  frege91  38765  frege97  38771  frege109  38783  frege130  38804  neik0pk1imk0  38862  axc11next  39123  pm13.192  39127  pm14.24  39149  gen11  39356  trsspwALT2  39560  snssiALT  39574  sstrALT2  39581  en3lpVD  39591  sspwimp  39665  sspwimpcf  39667  sspwimpALT  39672  ax6e2ndeqALT  39678  rnmptpr  39864  ssmapsn  39912  infnsuprnmpt  39965  uzinico  40284  icccncfext  40597  itgsinexplem1  40666  sge0resplit  41119  hoidmvlelem1  41308  hspdifhsp  41329  smflimsuplem7  41531  dfatcolem  41861  iccpartdisj  41965  zrinitorngc  42585  zrtermorngc  42586  zrtermoringc  42655  setrec2fun  43024  elsetrecslem  43030  setrecsss  43032  setrecsres  43033  0setrec  43035
  Copyright terms: Public domain W3C validator