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

Theorem alrimiv 1895
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2113 and 19.21v 1908. (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 1879 . 2 (𝜑 → ∀𝑥𝜑)
2 alrimiv.1 . 2 (𝜑𝜓)
31, 2alrimih 1791 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem is referenced by:  alrimivv  1896  nexdvOLD  1905  nfdvOLD  1930  cbvalivw  1980  equvelv  2005  aevlem0  2022  aev  2025  hbaevg  2026  aev2ALT  2029  nf5dv  2065  euequ1  2504  axext4  2635  eqrdv  2649  abbi2dv  2771  elex2  3247  elex22  3248  spcimdv  3321  pm13.183  3376  moeq3  3416  sbc2or  3477  sbcthdv  3484  sbcimdv  3531  sbcimdvOLD  3532  ssrdv  3642  ss2abdv  3708  abssdv  3709  dfnfc2  4486  dfnfc2OLD  4487  intab  4539  iuneq12df  4576  dfiin2g  4585  disjss1  4658  mpteq12dva  4765  axsep  4813  el  4877  reusv1OLD  4897  reusv2lem1  4898  reusv2lem2  4899  reusv2lem2OLD  4900  euotd  5004  ssrelrel  5254  issref  5544  asymref2  5548  iotaval  5900  iota5  5909  iotabidv  5910  funmo  5942  funco  5966  funun  5970  fununfun  5972  fununi  6002  nfunsn  6263  fvn0ssdmfun  6390  f1oresrab  6435  funoprabg  6801  tfisi  7100  limom  7122  funcnvuni  7161  1stconst  7310  2ndconst  7311  frxp  7332  fnwelem  7337  seqomlem2  7591  iserd  7813  findcard3  8244  frfi  8246  fiint  8278  dffi2  8370  hartogslem1  8488  wdomd  8527  ixpiunwdom  8537  rankval3b  8727  fseqenlem2  8886  dfac3  8982  dfac5  8989  dfac2  8991  dfac8  8995  dfac9  8996  dfacacn  9001  dfac13  9002  kmlem1  9010  kmlem6  9015  kmlem13  9022  fin23lem32  9204  axdc2lem  9308  zornn0g  9365  brdom6disj  9392  fpwwe2lem11  9500  fpwwe2lem12  9501  fpwwe2lem13  9502  hargch  9533  alephgch  9534  nqpr  9874  reclem2pr  9908  cshwsexa  13616  rtrclreclem4  13845  dfrtrcl2  13846  relexpindlem  13847  shftfn  13857  ramub  15764  ramcl  15780  imasaddfnlem  16235  imasvscafn  16244  mrieqv2d  16346  mreexexd  16355  mreexexdOLD  16356  invfun  16471  joinfval  17048  meetfval  17062  mreclatBAD  17234  letsr  17274  efgval  18176  efgi  18178  efgi2  18184  gsumval3lem2  18353  gsumzaddlem  18367  pgpfac1lem5  18524  islbs3  19203  lbsextlem4  19209  mplsubglem  19482  mpllsslem  19483  cssmre  20085  obslbs  20122  tgcl  20821  indistopon  20853  ppttop  20859  epttop  20861  mretopd  20944  toponmre  20945  neissex  20979  neiptoptop  20983  lmfun  21233  2ndcdisj  21307  1stccnp  21313  kgentopon  21389  dfac14  21469  ptcnp  21473  uptx  21476  ptrescn  21490  qtoptop2  21550  filconn  21734  filssufilg  21762  rnelfmlem  21803  alexsubALTlem2  21899  cnextfun  21915  utoptop  22085  prdsxmslem2  22381  vitalilem3  23424  mbfposr  23464  mbfinf  23477  i1fd  23493  itg1climres  23526  perfdvf  23712  taylf  24160  mptelee  25820  upgr1eopALT  26057  upgrspanop  26234  umgrspanop  26235  usgrspanop  26236  cplgrop  26389  umgr2v2enb1  26478  iswspthsnon  26806  clwwlknon1loop  27073  ex-natded9.26  27406  ex-natded9.26-2  27407  aevdemo  27447  nmcexi  29013  moimd  29454  rabeqsnd  29468  iuneq12daf  29499  abfmpeld  29582  abfmpel  29583  fpwrelmap  29636  rngurd  29916  bnj1143  30987  bnj1379  31027  bnj149  31071  mclsssvlem  31585  ssmclslem  31588  mclsax  31592  mclsind  31593  dfpo2  31771  dfon2lem6  31817  dfon2lem8  31819  dfon2lem9  31820  dfon2  31821  trer  32435  finminlem  32437  neibastop1  32479  neibastop3  32482  unblimceq0  32623  unbdqndv1  32624  knoppndv  32650  bj-alsb  32750  bj-ssbequ1  32769  bj-ssbid1ALT  32773  bj-eqs  32788  bj-elequ2g  32791  bj-sb  32802  bj-abbi2dv  32905  bj-axsep  32918  bj-el  32921  bj-spcimdv  33009  bj-spcimdvv  33010  bj-csbprc  33029  bj-cleq  33074  bj-ismooredr  33189  exellimddv  33323  wl-cbv3vv  33437  fin2so  33526  poimirlem17  33556  mblfinlem3  33578  ismblfin  33580  itg2addnc  33594  upixp  33654  mpt2bi123f  34101  mptbi12f  34105  trcoss  34372  prter1  34483  axc11n-16  34542  ax12eq  34545  ax12el  34546  ismrcd1  37578  ttac  37920  fnwe2  37940  aomclem6  37946  dfac11  37949  dfac21  37953  hbtlem2  38011  cllem0  38188  clss2lem  38235  mptrcllem  38237  iunrelexpmin1  38317  iunrelexpmin2  38321  iunrelexpuztr  38328  dftrcl3  38329  brtrclfv2  38336  dfrtrcl3  38342  psshepw  38399  frege91  38565  frege97  38571  frege109  38583  frege130  38604  neik0pk1imk0  38662  sbeqalbi  38918  axc11next  38924  pm13.192  38928  pm14.24  38950  gen11  39158  trsspwALT2  39363  snssiALT  39377  sstrALT2  39384  en3lpVD  39394  sspwimp  39468  sspwimpcf  39470  sspwimpALT  39475  ax6e2ndeqALT  39481  rnmptpr  39672  ssmapsn  39722  infnsuprnmpt  39779  uzinico  40105  icccncfext  40418  itgsinexplem1  40487  sge0resplit  40941  hoidmvlelem1  41130  hspdifhsp  41151  smflimsuplem7  41353  funressnfv  41529  iccpartdisj  41698  zrinitorngc  42325  zrtermorngc  42326  zrtermoringc  42395  setrec2fun  42764  elsetrecslem  42770  setrecsss  42772  setrecsres  42773  0setrec  42775
  Copyright terms: Public domain W3C validator