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

Theorem alrimiv 1853
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2073 and 19.21v 1866. (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 1837 . 2 (𝜑 → ∀𝑥𝜑)
2 alrimiv.1 . 2 (𝜑𝜓)
31, 2alrimih 1749 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1479
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1720  ax-4 1735  ax-5 1837
This theorem is referenced by:  alrimivv  1854  nexdvOLD  1863  nfdvOLD  1871  cbvalivw  1932  equvelv  1961  aevlem0  1978  aev  1981  hbaevg  1982  aev2ALT  1985  nf5dv  2023  euequ1  2474  axext4  2604  eqrdv  2618  abbi2dv  2740  elex2  3211  elex22  3212  spcimdv  3285  pm13.183  3338  moeq3  3377  sbc2or  3438  sbcthdv  3445  sbcimdv  3492  sbcimdvOLD  3493  ssrdv  3601  ss2abdv  3667  abssdv  3668  dfnfc2  4445  dfnfc2OLD  4446  intab  4498  iuneq12df  4535  dfiin2g  4544  disjss1  4617  mpteq12dva  4723  axsep  4771  el  4838  reusv1OLD  4858  reusv2lem1  4859  reusv2lem2  4860  reusv2lem2OLD  4861  euotd  4965  ssrelrel  5210  issref  5497  asymref2  5501  iotaval  5850  iota5  5859  iotabidv  5860  funmo  5892  funco  5916  funun  5920  fununfun  5922  fununi  5952  nfunsn  6212  fvn0ssdmfun  6336  f1oresrab  6381  funoprabg  6744  tfisi  7043  limom  7065  funcnvuni  7104  1stconst  7250  2ndconst  7251  frxp  7272  fnwelem  7277  seqomlem2  7531  iserd  7753  findcard3  8188  frfi  8190  fiint  8222  dffi2  8314  hartogslem1  8432  wdomd  8471  ixpiunwdom  8481  rankval3b  8674  fseqenlem2  8833  dfac3  8929  dfac5  8936  dfac2  8938  dfac8  8942  dfac9  8943  dfacacn  8948  dfac13  8949  kmlem1  8957  kmlem6  8962  kmlem13  8969  fin23lem32  9151  axdc2lem  9255  zornn0g  9312  brdom6disj  9339  fpwwe2lem11  9447  fpwwe2lem12  9448  fpwwe2lem13  9449  hargch  9480  alephgch  9481  nqpr  9821  reclem2pr  9855  cshwsexa  13551  rtrclreclem4  13782  dfrtrcl2  13783  relexpindlem  13784  shftfn  13794  ramub  15698  ramcl  15714  imasaddfnlem  16169  imasvscafn  16178  mrieqv2d  16280  mreexexd  16289  mreexexdOLD  16290  invfun  16405  joinfval  16982  meetfval  16996  mreclatBAD  17168  letsr  17208  efgval  18111  efgi  18113  efgi2  18119  gsumval3lem2  18288  gsumzaddlem  18302  pgpfac1lem5  18459  islbs3  19136  lbsextlem4  19142  mplsubglem  19415  mpllsslem  19416  cssmre  20018  obslbs  20055  tgcl  20754  indistopon  20786  ppttop  20792  epttop  20794  mretopd  20877  toponmre  20878  neissex  20912  neiptoptop  20916  lmfun  21166  2ndcdisj  21240  1stccnp  21246  kgentopon  21322  dfac14  21402  ptcnp  21406  uptx  21409  ptrescn  21423  qtoptop2  21483  filconn  21668  filssufilg  21696  rnelfmlem  21737  alexsubALTlem2  21833  cnextfun  21849  utoptop  22019  prdsxmslem2  22315  vitalilem3  23360  mbfposr  23400  mbfinf  23413  i1fd  23429  itg1climres  23462  perfdvf  23648  taylf  24096  mptelee  25756  upgr1eopALT  25993  upgrspanop  26170  umgrspanop  26171  usgrspanop  26172  cplgrop  26314  umgr2v2enb1  26403  ex-natded9.26  27246  ex-natded9.26-2  27247  aevdemo  27287  nmcexi  28855  moimd  29298  rabeqsnd  29314  iuneq12daf  29345  abfmpeld  29427  abfmpel  29428  fpwrelmap  29482  rngurd  29762  bnj145OLD  30769  bnj1143  30835  bnj1379  30875  bnj149  30919  mclsssvlem  31433  ssmclslem  31436  mclsax  31440  mclsind  31441  dfpo2  31620  dfon2lem6  31667  dfon2lem8  31669  dfon2lem9  31670  dfon2  31671  trer  32285  finminlem  32287  neibastop1  32329  neibastop3  32332  unblimceq0  32473  unbdqndv1  32474  knoppndv  32500  bj-alsb  32600  bj-ssbequ1  32619  bj-ssbid1ALT  32623  bj-eqs  32638  bj-elequ2g  32641  bj-sb  32652  bj-abbi2dv  32755  bj-axsep  32768  bj-el  32771  bj-spcimdv  32859  bj-spcimdvv  32860  bj-csbprc  32879  bj-cleq  32924  bj-ismooredr  33039  exellimddv  33164  wl-cbv3vv  33278  fin2so  33367  poimirlem17  33397  mblfinlem3  33419  ismblfin  33421  itg2addnc  33435  upixp  33495  mpt2bi123f  33942  mptbi12f  33946  prter1  33983  axc11n-16  34042  ax12eq  34045  ax12el  34046  ismrcd1  37080  ttac  37422  fnwe2  37442  aomclem6  37448  dfac11  37451  dfac21  37455  hbtlem2  37513  cllem0  37690  clss2lem  37737  mptrcllem  37739  iunrelexpmin1  37819  iunrelexpmin2  37823  iunrelexpuztr  37830  dftrcl3  37831  brtrclfv2  37838  dfrtrcl3  37844  psshepw  37902  frege91  38068  frege97  38074  frege109  38086  frege130  38107  neik0pk1imk0  38165  sbeqalbi  38421  axc11next  38427  pm13.192  38431  pm14.24  38453  sbcssOLD  38576  gen11  38661  trsspwALT2  38866  snssiALT  38883  sstrALT2  38890  en3lpVD  38900  sspwimp  38974  sspwimpcf  38976  sspwimpALT  38981  ax6e2ndeqALT  38987  rnmptpr  39174  ssmapsn  39224  infnsuprnmpt  39281  uzinico  39590  icccncfext  39863  itgsinexplem1  39932  sge0resplit  40386  hoidmvlelem1  40572  hspdifhsp  40593  smflimsuplem7  40795  funressnfv  40971  iccpartdisj  41137  zrinitorngc  41765  zrtermorngc  41766  zrtermoringc  41835  setrec2fun  42204  elsetrecslem  42209  0setrec  42212
  Copyright terms: Public domain W3C validator