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

Theorem alrimiv 1919
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 2197 and 19.21v 1931. (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 1902 . 2 (𝜑 → ∀𝑥𝜑)
2 alrimiv.1 . 2 (𝜑𝜓)
31, 2alrimih 1815 1 (𝜑 → ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem is referenced by:  alrimivv  1920  cbvalivw  2005  aevlem0  2050  aev  2053  aev2  2054  stdpc4  2064  sbimdv  2074  sbbidv  2075  elequ2g  2122  cbv3v2  2233  nexmo  2616  moimdv  2622  mobidv  2626  eubidv  2665  euequ  2676  eqrdv  2816  abbidv  2882  abbi2dvOLD  2948  elex2  3514  elex22  3515  pm13.183  3656  pm13.183OLD  3657  moeq3  3700  sbc2or  3778  sbcthdv  3785  sbcimdv  3840  ssrdv  3970  ss2abdv  4041  abssdv  4042  rabsn  4649  dfnfc2  4848  intab  4897  iuneq12df  4936  dfiin2g  4948  mpteq12dva  5141  el  5261  reusv2lem1  5289  reusv2lem2  5290  axprlem3  5316  sbcop1  5370  euotd  5394  ssrelrel  5662  asymref2  5970  iotaval  6322  iota5  6331  iotabidv  6332  funmo  6364  funco  6388  funun  6393  fununfun  6395  fununi  6422  nfunsn  6700  fvn0ssdmfun  6834  f1oresrab  6881  0mpo0  7226  funoprabg  7262  tfisi  7562  limom  7584  funcnvuni  7625  1stconst  7784  2ndconst  7785  frxp  7809  fnwelem  7814  seqomlem2  8076  iserd  8304  findcard3  8749  frfi  8751  fiint  8783  dffi2  8875  hartogslem1  8994  wdomd  9033  ixpiunwdom  9043  rankval3b  9243  fseqenlem2  9439  dfac3  9535  dfac5  9542  dfac2b  9544  dfac8  9549  dfac9  9550  dfacacn  9555  dfac13  9556  kmlem1  9564  kmlem6  9569  kmlem13  9576  fin23lem32  9754  axdc2lem  9858  zornn0g  9915  fpwwe2lem11  10050  fpwwe2lem12  10051  fpwwe2lem13  10052  hargch  10083  alephgch  10084  nqpr  10424  reclem2pr  10458  hashgt23el  13773  cshwsexa  14174  rtrclreclem4  14408  dfrtrcl2  14409  relexpindlem  14410  shftfn  14420  ramub  16337  ramcl  16353  imasaddfnlem  16789  imasvscafn  16798  mrieqv2d  16898  mreexexd  16907  invfun  17022  joinfval  17599  meetfval  17613  mreclatBAD  17785  letsr  17825  efgval  18772  efgi  18774  efgi2  18780  gsumval3lem2  18955  gsumzaddlem  18970  pgpfac1lem5  19130  islbs3  19856  lbsextlem4  19862  mplsubglem  20142  mpllsslem  20143  cssmre  20765  obslbs  20802  tgcl  21505  indistopon  21537  ppttop  21543  epttop  21545  mretopd  21628  toponmre  21629  neissex  21663  neiptoptop  21667  lmfun  21917  2ndcdisj  21992  1stccnp  21998  kgentopon  22074  dfac14  22154  ptcnp  22158  uptx  22161  ptrescn  22175  qtoptop2  22235  filconn  22419  filssufilg  22447  rnelfmlem  22488  alexsubALTlem2  22584  cnextfun  22600  utoptop  22770  prdsxmslem2  23066  vitalilem3  24138  mbfposr  24180  mbfinf  24193  i1fd  24209  itg1climres  24242  perfdvf  24428  taylf  24876  mptelee  26608  upgr1eopALT  26829  upgrspanop  27006  umgrspanop  27007  usgrspanop  27008  cplgrop  27146  umgr2v2enb1  27235  clwwlknon1loop  27804  wlkl0  28073  ex-natded9.26  28125  ex-natded9.26-2  28126  aevdemo  28166  nmcexi  29730  rabeqsnd  30191  iuneq12daf  30236  abfmpeld  30327  abfmpel  30328  fpwrelmap  30395  rngurd  30784  bnj1143  31961  bnj1379  32001  bnj149  32046  loop1cycl  32281  satffunlem1lem1  32546  satffunlem2lem1  32548  prv0  32574  mclsssvlem  32706  ssmclslem  32709  mclsax  32713  mclsind  32714  dfpo2  32888  dfon2lem6  32930  dfon2lem8  32932  dfon2lem9  32933  dfon2  32934  frrlem9  33028  trer  33561  finminlem  33563  neibastop1  33604  neibastop3  33607  unbdqndv1  33744  knoppndv  33770  bj-ssbid1ALT  33895  bj-eqs  33905  bj-sb  33918  bj-nnfbd  33955  bj-spcimdv  34108  bj-spcimdvv  34109  bj-csbprc  34123  curryset  34154  currysetlem3  34157  bj-cleq  34171  exellimddv  34508  finorwe  34545  wl-motae  34637  wl-cbvalsbi  34666  fin2so  34760  poimirlem17  34790  mblfinlem3  34812  ismblfin  34814  itg2addnc  34827  upixp  34885  mpobi123f  35321  mptbi12f  35325  trcoss  35602  prter1  35895  axc11n-16  35954  ax12eq  35957  ax12el  35958  sn-axprlem3  38987  sn-el  38988  ismrcd1  39173  ttac  39511  fnwe2  39531  aomclem6  39537  dfac11  39540  dfac21  39544  hbtlem2  39602  cllem0  39803  clss2lem  39849  mptrcllem  39851  iunrelexpmin1  39931  iunrelexpmin2  39935  iunrelexpuztr  39942  dftrcl3  39943  brtrclfv2  39950  dfrtrcl3  39956  psshepw  40012  frege91  40178  frege97  40184  frege109  40196  frege130  40217  grumnudlem  40498  axc11next  40615  pm13.192  40619  pm14.24  40641  gen11  40827  trsspwALT2  41030  snssiALT  41039  sstrALT2  41046  en3lpVD  41056  sspwimp  41129  sspwimpcf  41131  sspwimpALT  41136  ax6e2ndeqALT  41142  ssmapsn  41355  infnsuprnmpt  41398  uzinico  41712  icccncfext  42046  itgsinexplem1  42115  sge0resplit  42565  hoidmvlelem1  42754  hspdifhsp  42775  smflimsuplem7  42977  dfatcolem  43331  iccpartdisj  43474  sbcpr  43560  zrinitorngc  44199  zrtermorngc  44200  zrtermoringc  44269  setrec2fun  44723  elsetrecslem  44729  setrecsss  44731  setrecsres  44732  0setrec  44734
  Copyright terms: Public domain W3C validator