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

Theorem alrimiv 1719
Description: Inference form of Theorem 19.21 of [Margaris] p. 90. See 19.21 1905 and 19.21v 1729. (Contributed by NM, 21-Jun-1993.)
Hypothesis
Ref Expression
alrimiv.1
Assertion
Ref Expression
alrimiv
Distinct variable group:   ,

Proof of Theorem alrimiv
StepHypRef Expression
1 ax-5 1704 . 2
2 alrimiv.1 . 2
31, 2alrimih 1642 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  A.wal 1393
This theorem is referenced by:  alrimivv  1720  nfdv  1727  cbvalivw  1789  axc11n-16  2268  ax12eq  2271  ax12el  2272  euequ1  2288  axext4  2439  eqrdv  2454  abbi2dv  2594  abbi1dvOLD  2596  elex2  3121  elex22  3122  spcimdv  3191  pm13.183  3240  moeq3  3276  sbc2or  3336  sbcthdv  3343  sbcimdv  3396  sbcimdvOLD  3397  ssrdv  3509  ss2abdv  3572  abssdv  3573  dfnfc2  4267  intssOLD  4308  intab  4317  iuneq12df  4354  dfiin2g  4363  disjss1  4428  mpteq12dva  4529  axsep  4572  el  4634  reusv1  4652  reusv2lem1  4653  reusv2lem2  4654  euotd  4753  ssrelrel  5108  issref  5385  asymref2  5389  iotaval  5567  iota5  5576  iotabidv  5577  funmo  5609  funco  5631  funun  5635  fununfun  5637  fununi  5659  nfunsn  5902  fvn0ssdmfun  6022  f1oresrab  6063  funoprabg  6401  tfisi  6693  limom  6715  funcnvuni  6753  1stconst  6888  2ndconst  6889  frxp  6910  fnwelem  6915  seqomlem2  7135  iserd  7356  findcard3  7783  frfi  7785  fiint  7817  dffi2  7903  hartogslem1  7988  wdomd  8028  ixpiunwdom  8038  sucprcregOLD  8047  rankval3b  8265  fseqenlem2  8427  dfac3  8523  dfac5  8530  dfac2  8532  dfac8  8536  dfac9  8537  dfacacn  8542  dfac13  8543  kmlem1  8551  kmlem6  8556  kmlem13  8563  fin23lem32  8745  axdc2lem  8849  zornn0g  8906  brdom6disj  8931  fpwwe2lem11  9039  fpwwe2lem12  9040  fpwwe2lem13  9041  hargch  9072  alephgch  9073  nqpr  9413  reclem2pr  9447  cshwsexa  12792  shftfn  12906  ramub  14531  ramcl  14547  imasaddfnlem  14925  imasvscafn  14934  mrieqv2d  15036  mreexexd  15045  invfun  15158  joinfval  15631  meetfval  15645  mreclatBAD  15817  letsr  15857  efgval  16735  efgi  16737  efgi2  16743  gsumval3OLD  16908  gsumval3lem2  16910  gsumzaddlem  16934  gsumzaddlemOLD  16936  pgpfac1lem5  17130  islbs3  17801  lbsextlem4  17807  mplsubglem  18093  mpllsslem  18094  mplsubglemOLD  18095  mpllsslemOLD  18096  cssmre  18724  obslbs  18761  tgcl  19471  indistopon  19502  ppttop  19508  epttop  19510  mretopd  19593  toponmre  19594  neissex  19628  neiptoptop  19632  lmfun  19882  2ndcdisj  19957  1stccnp  19963  kgentopon  20039  dfac14  20119  ptcnp  20123  uptx  20126  ptrescn  20140  qtoptop2  20200  filcon  20384  filssufilg  20412  rnelfmlem  20453  alexsubALTlem2  20548  cnextfun  20564  utoptop  20737  prdsxmslem2  21032  vitalilem3  22019  mbfposr  22059  mbfinf  22072  i1fd  22088  itg1climres  22121  perfdvf  22307  taylf  22756  mptelee  24198  ex-natded9.26  25140  ex-natded9.26-2  25141  nmcexi  26945  moimd  27385  iuneq12daf  27425  abfmpeld  27492  abfmpel  27493  fpwrelmap  27556  rngurd  27778  mclsssvlem  28922  ssmclslem  28925  mclsax  28929  mclsind  28930  relexpindlem  29062  rtrclreclem.min  29070  dfrtrcl2  29071  dfpo2  29184  dfon2lem6  29220  dfon2lem8  29222  dfon2lem9  29223  dfon2  29224  fin2so  30040  mblfinlem3  30053  ismblfin  30055  itg2addnc  30069  trer  30134  finminlem  30136  neibastop1  30177  neibastop3  30180  upixp  30220  mpt2bi123f  30571  mptbi12f  30575  prter1  30620  ismrcd1  30630  ttac  30978  fnwe2  30999  aomclem6  31005  dfac11  31008  dfac21  31012  hbtlem2  31073  sbeqalbi  31307  axc11next  31313  pm13.192  31317  pm14.24  31339  icccncfext  31690  itgsinexplem1  31752  funressnfv  32213  zrinitorngc  32808  zrtermorngc  32809  zrtermoringc  32878  sbcssOLD  33313  gen11  33402  trsspwALT2  33617  snssiALT  33628  sstrALT2  33635  en3lpVD  33645  sspwimp  33718  sspwimpcf  33720  sspwimpALT  33725  ax6e2ndeqALT  33731  bnj145OLD  33782  bnj1143  33849  bnj1379  33889  bnj149  33933  bj-elequ2g  34237  bj-abbi2dv  34366  bj-abbi1dv  34367  bj-axsep  34379  bj-el  34382  bj-csbprc  34476  bj-cleq  34519  cllem0  37751  psshepw  37811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-gen 1618  ax-4 1631  ax-5 1704
  Copyright terms: Public domain W3C validator