NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  eximdv Unicode version

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

Proof of Theorem eximdv
StepHypRef Expression
1 ax-17 1616 . 2
2 alimdv.1 . 2
31, 2eximdh 1588 1
Colors of variables: wff setvar class
Syntax hints:   wi 4  wex 1541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616
This theorem depends on definitions:  df-bi 177  df-ex 1542
This theorem is referenced by:  2eximdv  1624  exlimdv  1636  ax12olem2  1928  moim  2250  morimv  2252  reximdv2  2723  cgsexg  2890  spc3egv  2943  euind  3023  ssel  3267  reupick  3539  reximdva0  3561  uniss  3912  nnpw1ex  4484  coss1  4872  coss2  4873  dmss  4906  dmcosseq  4973  funssres  5144  fv3  5341  dffo4  5423  dffo5  5424  fvclss  5462  mapsn  6026  ncspw1eu  6159  taddc  6229  fnfreclem3  6319
  Copyright terms: Public domain W3C validator