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

Theorem rexlimiv 2601
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 1539 . 2 𝑥𝜓
2 rexlimiv.1 . 2 (𝑥𝐴 → (𝜑𝜓))
31, 2rexlimi 2600 1 (∃𝑥𝐴 𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2160  wrex 2469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-i5r 1546
This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473  df-rex 2474
This theorem is referenced by:  rexlimiva  2602  rexlimivw  2603  rexlimivv  2613  r19.36av  2641  r19.44av  2649  r19.45av  2650  rexn0  3536  uniss2  3855  elres  4961  ssimaex  5597  mpoexw  6237  tfrlem5  6338  tfrlem8  6342  ecoptocl  6647  mapsn  6715  elixpsn  6760  ixpsnf1o  6761  findcard  6915  findcard2  6916  findcard2s  6917  fiintim  6956  prnmaddl  7518  0re  7986  cnegexlem2  8162  0cnALT  8176  bndndx  9204  uzn0  9572  ublbneg  9642  rexanuz2  11031  opnneiid  14116  2sqlem2  14915  bj-inf2vnlem2  15176
  Copyright terms: Public domain W3C validator