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

Theorem rexlimdva 2738
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)
Hypothesis
Ref Expression
rexlimdva.1 ((φ x A) → (ψχ))
Assertion
Ref Expression
rexlimdva (φ → (x A ψχ))
Distinct variable groups:   φ,x   χ,x
Allowed substitution hints:   ψ(x)   A(x)

Proof of Theorem rexlimdva
StepHypRef Expression
1 rexlimdva.1 . . 3 ((φ x A) → (ψχ))
21ex 423 . 2 (φ → (x A → (ψχ)))
32rexlimdv 2737 1 (φ → (x A ψχ))
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:  rexlimdvaa  2739  rexlimivv  2743  rexlimdvv  2744  pw1disj  4167  leltfintr  4458  ncfinlower  4483  tfin11  4493  tfinpw1  4494  nnpweq  4523  sfin112  4529  sfindbl  4530  vfinspss  4551  vfinspeqtncv  4553  phi11lem1  4595  foco2  5426  f1elima  5474  ectocld  5991  ncssfin  6151  nntccl  6170  dflec2  6210  leaddc1  6214  leconnnc  6218  tlecg  6230  letc  6231  ce2le  6233  ce0lenc1  6239  nclenn  6249  lemuc1  6253  lecadd2  6266  ncslesuc  6267  nnc3n3p1  6278  nchoicelem17  6305  nchoicelem19  6307  nchoice  6308  dmfrec  6316  fnfreclem3  6319
  Copyright terms: Public domain W3C validator