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

Theorem rexlimdvva 2745
 Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
rexlimdvva.1
Assertion
Ref Expression
rexlimdvva
Distinct variable groups:   ,,   ,,   ,
Allowed substitution hints:   (,)   ()   (,)

Proof of Theorem rexlimdvva
StepHypRef Expression
1 rexlimdvva.1 . . 3
21ex 423 . 2
32rexlimdvv 2744 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 358   wcel 1710  wrex 2615 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  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-ral 2619  df-rex 2620 This theorem is referenced by:  nnsucelr  4428  nndisjeq  4429  prepeano4  4451  ltfintr  4459  ncfinlower  4483  tfindi  4496  tfinsuc  4498  nnadjoin  4520  nnpweq  4523  sfindbl  4530  tfinnn  4534  vfinspsslem1  4550  ncdisjun  6136  peano4nc  6150  ncspw1eu  6159  ce0addcnnul  6179  sbth  6206  dflec2  6210  lectr  6211
 Copyright terms: Public domain W3C validator