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

Theorem alrimiv 1842
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2062 and 19.21v 1855. (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 1827 . 2 (𝜑 → ∀𝑥𝜑)
2 alrimiv.1 . 2 (𝜑𝜓)
31, 2alrimih 1741 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1713  ax-4 1728  ax-5 1827
This theorem is referenced by:  alrimivv  1843  nexdvOLD  1852  nfdvOLD  1860  cbvalivw  1921  equvelv  1950  aevlem0  1967  aev  1970  hbaevg  1971  aev2ALT  1974  nf5dv  2012  euequ1  2464  axext4  2594  eqrdv  2608  abbi2dv  2729  elex2  3189  elex22  3190  spcimdv  3263  pm13.183  3313  moeq3  3350  sbc2or  3411  sbcthdv  3418  sbcimdv  3465  sbcimdvOLD  3466  ssrdv  3574  ss2abdv  3638  abssdv  3639  dfnfc2  4390  dfnfc2OLD  4391  intab  4442  iuneq12df  4480  dfiin2g  4489  disjss1  4559  mpteq12dva  4662  axsep  4708  el  4773  reusv1OLD  4793  reusv2lem1  4794  reusv2lem2  4795  reusv2lem2OLD  4796  euotd  4900  ssrelrel  5143  issref  5428  asymref2  5432  iotaval  5779  iota5  5788  iotabidv  5789  funmo  5820  funco  5842  funun  5846  fununfun  5848  fununi  5878  nfunsn  6135  fvn0ssdmfun  6258  f1oresrab  6302  funoprabg  6657  tfisi  6950  limom  6972  funcnvuni  7012  1stconst  7152  2ndconst  7153  frxp  7174  fnwelem  7179  seqomlem2  7433  iserd  7655  findcard3  8088  frfi  8090  fiint  8122  dffi2  8212  hartogslem1  8330  wdomd  8369  ixpiunwdom  8379  rankval3b  8572  fseqenlem2  8731  dfac3  8827  dfac5  8834  dfac2  8836  dfac8  8840  dfac9  8841  dfacacn  8846  dfac13  8847  kmlem1  8855  kmlem6  8860  kmlem13  8867  fin23lem32  9049  axdc2lem  9153  zornn0g  9210  brdom6disj  9235  fpwwe2lem11  9341  fpwwe2lem12  9342  fpwwe2lem13  9343  hargch  9374  alephgch  9375  nqpr  9715  reclem2pr  9749  cshwsexa  13421  rtrclreclem4  13649  dfrtrcl2  13650  relexpindlem  13651  shftfn  13661  ramub  15555  ramcl  15571  imasaddfnlem  16011  imasvscafn  16020  mrieqv2d  16122  mreexexd  16131  mreexexdOLD  16132  invfun  16247  joinfval  16824  meetfval  16838  mreclatBAD  17010  letsr  17050  efgval  17953  efgi  17955  efgi2  17961  gsumval3lem2  18130  gsumzaddlem  18144  pgpfac1lem5  18301  islbs3  18976  lbsextlem4  18982  mplsubglem  19255  mpllsslem  19256  cssmre  19856  obslbs  19893  tgcl  20584  indistopon  20615  ppttop  20621  epttop  20623  mretopd  20706  toponmre  20707  neissex  20741  neiptoptop  20745  lmfun  20995  2ndcdisj  21069  1stccnp  21075  kgentopon  21151  dfac14  21231  ptcnp  21235  uptx  21238  ptrescn  21252  qtoptop2  21312  filcon  21497  filssufilg  21525  rnelfmlem  21566  alexsubALTlem2  21662  cnextfun  21678  utoptop  21848  prdsxmslem2  22144  vitalilem3  23185  mbfposr  23225  mbfinf  23238  i1fd  23254  itg1climres  23287  perfdvf  23473  taylf  23919  mptelee  25575  upgr1eopALT  25783  ex-natded9.26  26668  ex-natded9.26-2  26669  aevdemo  26709  nmcexi  28269  moimd  28710  iuneq12daf  28756  abfmpeld  28834  abfmpel  28835  fpwrelmap  28896  rngurd  29119  bnj145OLD  30049  bnj1143  30115  bnj1379  30155  bnj149  30199  mclsssvlem  30713  ssmclslem  30716  mclsax  30720  mclsind  30721  dfpo2  30898  dfon2lem6  30937  dfon2lem8  30939  dfon2lem9  30940  dfon2  30941  trer  31480  finminlem  31482  neibastop1  31524  neibastop3  31527  unblimceq0  31668  unbdqndv1  31669  knoppndv  31695  bj-alsb  31814  bj-ssbequ1  31833  bj-ssbid1ALT  31837  bj-eqs  31850  bj-elequ2g  31853  bj-sb  31864  bj-abbi2dv  31968  bj-axsep  31981  bj-el  31984  bj-spcimdv  32078  bj-csbprc  32096  bj-cleq  32142  exellimddv  32369  wl-cbv3vv  32486  fin2so  32566  poimirlem17  32596  mblfinlem3  32618  ismblfin  32620  itg2addnc  32634  upixp  32694  mpt2bi123f  33141  mptbi12f  33145  prter1  33182  axc11n-16  33241  ax12eq  33244  ax12el  33245  ismrcd1  36279  ttac  36621  fnwe2  36641  aomclem6  36647  dfac11  36650  dfac21  36654  hbtlem2  36713  cllem0  36890  clss2lem  36937  mptrcllem  36939  iunrelexpmin1  37019  iunrelexpmin2  37023  iunrelexpuztr  37030  dftrcl3  37031  brtrclfv2  37038  dfrtrcl3  37044  psshepw  37102  frege91  37268  frege97  37274  frege109  37286  frege130  37307  neik0pk1imk0  37365  sbeqalbi  37623  axc11next  37629  pm13.192  37633  pm14.24  37655  sbcssOLD  37777  gen11  37862  trsspwALT2  38068  snssiALT  38085  sstrALT2  38092  en3lpVD  38102  sspwimp  38176  sspwimpcf  38178  sspwimpALT  38183  ax6e2ndeqALT  38189  rnmptpr  38353  ssmapsn  38403  icccncfext  38773  itgsinexplem1  38845  sge0resplit  39299  hoidmvlelem1  39485  hspdifhsp  39506  funressnfv  39857  iccpartdisj  39975  upgrspanop  40521  umgrspanop  40522  usgrspanop  40523  cplgrop  40659  umgr2v2enb1  40742  zrinitorngc  41792  zrtermorngc  41793  zrtermoringc  41862  setrec2fun  42238  elsetrecslem  42243  0setrec  42246
  Copyright terms: Public domain W3C validator