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

Theorem alimdv 2017
 Description: Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by NM, 3-Apr-1994.)
Hypothesis
Ref Expression
alimdv.1
Assertion
Ref Expression
alimdv
Distinct variable group:   ,
Allowed substitution hints:   ()   ()

Proof of Theorem alimdv
StepHypRef Expression
1 nfv 1629 . 2
2 alimdv.1 . 2
31, 2alimd 1705 1
 Colors of variables: wff set class Syntax hints:   wi 6  wal 1532 This theorem is referenced by:  2alimdv  2019  moimv  2161  ralimdv2  2585  mo2icl  2881  sstr2  3107  reuss2  3355  ssuni  3749  disjss2  3893  disjss1  3896  disjiun  3910  disjss3  3919  frss  4253  alxfr  4438  dfwe2  4464  ordom  4556  ssrel  4683  ssrelrel  4694  fv2  5373  dff3  5525  iotaval  6154  findcard3  6985  dffi2  7060  indcardi  7552  zorn2lem4  8010  uzindi  10921  caubnd  11719  ramtlecl  12921  dfcon2  16977  2ndcdisj  17014  wilthlem3  20140  onsuct0  24054  domrngref  24225  bwt2  24758  pgapspf2  25219  psgnunilem4  26586  ax10ext  26772 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692 This theorem depends on definitions:  df-bi 179  df-nf 1540
 Copyright terms: Public domain W3C validator