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

Theorem rexlimdv 2737
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 14-Nov-2002.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
Hypothesis
Ref Expression
rexlimdv.1 (φ → (x A → (ψχ)))
Assertion
Ref Expression
rexlimdv (φ → (x A ψχ))
Distinct variable groups:   φ,x   χ,x
Allowed substitution hints:   ψ(x)   A(x)

Proof of Theorem rexlimdv
StepHypRef Expression
1 nfv 1619 . 2 xφ
2 nfv 1619 . 2 xχ
3 rexlimdv.1 . 2 (φ → (x A → (ψχ)))
41, 2, 3rexlimd 2735 1 (φ → (x A ψχ))
Colors of variables: wff setvar class
Syntax hints:  wi 4   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:  rexlimdva  2738  rexlimdv3a  2740  rexlimdvw  2741  rexlimdvv  2744  eqpw1uni  4330  nndisjeq  4429  ssfin  4470  nnpw1ex  4484  tfinltfinlem1  4500  sfin112  4529  sfintfin  4532  sfinltfin  4535  funcnvuni  5161  dffo3  5422  nclenn  6249  ncslesuc  6267
  Copyright terms: Public domain W3C validator