ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rexlimiv GIF version

Theorem rexlimiv 2444
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)
Hypothesis
Ref Expression
rexlimiv.1 (𝑥𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rexlimiv (∃𝑥𝐴 𝜑𝜓)
Distinct variable group:   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimiv
StepHypRef Expression
1 nfv 1437 . 2 𝑥𝜓
2 rexlimiv.1 . 2 (𝑥𝐴 → (𝜑𝜓))
31, 2rexlimi 2443 1 (∃𝑥𝐴 𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1409  wrex 2324
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-i5r 1444
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-ral 2328  df-rex 2329
This theorem is referenced by:  rexlimiva  2445  rexlimivw  2446  rexlimivv  2455  r19.36av  2478  r19.44av  2486  r19.45av  2487  rexn0  3346  uniss2  3638  elres  4673  ssimaex  5261  tfrlem5  5960  tfrlem8  5964  ecoptocl  6223  findcard  6375  findcard2  6376  findcard2s  6377  prnmaddl  6645  0re  7084  cnegexlem2  7249  0cnALT  7263  bndndx  8237  uzn0  8583  ublbneg  8644  rexanuz2  9817  bj-inf2vnlem2  10462
  Copyright terms: Public domain W3C validator