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

Theorem alrimiv 1928
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2206 and 19.21v 1940. (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 1911 . 2 (𝜑 → ∀𝑥𝜑)
2 alrimiv.1 . 2 (𝜑𝜓)
31, 2alrimih 1825 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1797  ax-4 1811  ax-5 1911
This theorem is referenced by:  alrimivv  1929  cbvalivw  2014  aevlem0  2059  aev  2062  aev2  2063  stdpc4  2073  sbimdv  2083  sbbidv  2084  elequ2g  2129  cbv3v2  2242  nexmo  2602  moimdv  2607  mobidv  2611  eubidv  2650  euequ  2661  eqrdv  2799  abbidv  2865  elex2  3466  elex22  3467  pm13.183  3609  moeq3  3654  sbc2or  3732  sbcthdv  3739  sbcimdv  3792  ssrdv  3924  ss2abdvOLD  3996  abssdv  3999  disj  4358  rabsn  4620  dfnfc2  4825  intab  4871  iuneq12df  4910  dfiin2g  4922  mpteq12dva  5117  el  5238  reusv2lem1  5267  reusv2lem2  5268  axprlem3  5294  sbcop1  5347  euotd  5371  ssrelrel  5637  asymref2  5948  iotaval  6302  iota5  6311  iotabidv  6312  funmo  6344  funco  6368  funun  6374  fununfun  6376  fununi  6403  nfunsn  6686  fvn0ssdmfun  6823  f1oresrab  6870  0mpo0  7220  funoprabg  7256  tfisi  7557  limom  7579  funcnvuni  7622  1stconst  7782  2ndconst  7783  frxp  7807  fnwelem  7812  seqomlem2  8074  iserd  8302  findcard3  8749  frfi  8751  fiint  8783  dffi2  8875  hartogslem1  8994  wdomd  9033  ixpiunwdom  9042  rankval3b  9243  fseqenlem2  9440  dfac3  9536  dfac5  9543  dfac2b  9545  dfac8  9550  dfac9  9551  dfacacn  9556  dfac13  9557  kmlem1  9565  kmlem6  9570  kmlem13  9577  fin23lem32  9759  axdc2lem  9863  zornn0g  9920  fpwwe2lem11  10055  fpwwe2lem12  10056  fpwwe2lem13  10057  hargch  10088  alephgch  10089  nqpr  10429  reclem2pr  10463  hashgt23el  13785  cshwsexa  14181  rtrclreclem4  14416  dfrtrcl2  14417  relexpindlem  14418  shftfn  14428  ramub  16343  ramcl  16359  imasaddfnlem  16797  imasvscafn  16806  mrieqv2d  16906  mreexexd  16915  invfun  17030  joinfval  17607  meetfval  17621  mreclatBAD  17793  letsr  17833  efgval  18839  efgi  18841  efgi2  18847  gsumval3lem2  19023  gsumzaddlem  19038  pgpfac1lem5  19198  islbs3  19924  lbsextlem4  19930  cssmre  20386  obslbs  20423  mplsubglem  20676  mpllsslem  20677  tgcl  21578  indistopon  21610  ppttop  21616  epttop  21618  mretopd  21701  toponmre  21702  neissex  21736  neiptoptop  21740  lmfun  21990  2ndcdisj  22065  1stccnp  22071  kgentopon  22147  dfac14  22227  ptcnp  22231  uptx  22234  ptrescn  22248  qtoptop2  22308  filconn  22492  filssufilg  22520  rnelfmlem  22561  alexsubALTlem2  22657  cnextfun  22673  utoptop  22844  prdsxmslem2  23140  vitalilem3  24218  mbfposr  24260  mbfinf  24273  i1fd  24289  itg1climres  24322  perfdvf  24510  taylf  24960  mptelee  26693  upgr1eopALT  26914  upgrspanop  27091  umgrspanop  27092  usgrspanop  27093  cplgrop  27231  umgr2v2enb1  27320  clwwlknon1loop  27887  wlkl0  28156  ex-natded9.26  28208  ex-natded9.26-2  28209  aevdemo  28249  nmcexi  29813  rabeqsnd  30275  iuneq12daf  30324  iinabrex  30336  abfmpeld  30421  abfmpel  30422  fpwrelmap  30499  rngurd  30911  ssmxidl  31054  zarclssn  31230  bnj1143  32176  bnj1379  32216  bnj149  32261  loop1cycl  32498  satffunlem1lem1  32763  satffunlem2lem1  32765  prv0  32791  mclsssvlem  32923  ssmclslem  32926  mclsax  32930  mclsind  32931  dfpo2  33105  dfon2lem6  33147  dfon2lem8  33149  dfon2lem9  33150  dfon2  33151  frrlem9  33245  trer  33778  finminlem  33780  neibastop1  33821  neibastop3  33824  unbdqndv1  33961  knoppndv  33987  bj-ssbid1ALT  34112  bj-eqs  34122  bj-sb  34135  bj-substw  34170  bj-nnfbd  34174  bj-spcimdv  34336  bj-spcimdvv  34337  bj-csbprc  34351  curryset  34382  currysetlem3  34385  bj-cleq  34399  exellimddv  34763  finorwe  34800  wl-motae  34919  wl-cbvalsbi  34949  fin2so  35043  poimirlem17  35073  mblfinlem3  35095  ismblfin  35097  itg2addnc  35110  upixp  35166  mpobi123f  35599  mptbi12f  35603  trcoss  35881  prter1  36174  axc11n-16  36233  ax12eq  36236  ax12el  36237  sbtd  39386  sn-axprlem3  39394  sn-el  39395  ismrcd1  39632  ttac  39970  fnwe2  39990  aomclem6  39996  dfac11  39999  dfac21  40003  hbtlem2  40061  cllem0  40258  clss2lem  40304  mptrcllem  40306  iunrelexpmin1  40402  iunrelexpmin2  40406  iunrelexpuztr  40413  dftrcl3  40414  brtrclfv2  40421  dfrtrcl3  40427  psshepw  40482  frege91  40648  frege97  40654  frege109  40666  frege130  40687  grumnudlem  40986  axc11next  41103  pm13.192  41107  pm14.24  41129  gen11  41315  trsspwALT2  41518  snssiALT  41527  sstrALT2  41534  en3lpVD  41544  sspwimp  41617  sspwimpcf  41619  sspwimpALT  41624  ax6e2ndeqALT  41630  ssmapsn  41838  infnsuprnmpt  41881  uzinico  42190  icccncfext  42522  itgsinexplem1  42589  sge0resplit  43038  hoidmvlelem1  43227  hspdifhsp  43248  smflimsuplem7  43450  dfatcolem  43804  iccpartdisj  43947  sbcpr  44031  zrinitorngc  44617  zrtermorngc  44618  zrtermoringc  44687  setrec2fun  45215  elsetrecslem  45221  setrecsss  45223  setrecsres  45224  0setrec  45226
  Copyright terms: Public domain W3C validator