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

Theorem rexlimiv 2581
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 1521 . 2 𝑥𝜓
2 rexlimiv.1 . 2 (𝑥𝐴 → (𝜑𝜓))
31, 2rexlimi 2580 1 (∃𝑥𝐴 𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 2141  wrex 2449
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528
This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453  df-rex 2454
This theorem is referenced by:  rexlimiva  2582  rexlimivw  2583  rexlimivv  2593  r19.36av  2621  r19.44av  2629  r19.45av  2630  rexn0  3512  uniss2  3825  elres  4925  ssimaex  5555  mpoexw  6190  tfrlem5  6291  tfrlem8  6295  ecoptocl  6598  mapsn  6666  elixpsn  6711  ixpsnf1o  6712  findcard  6864  findcard2  6865  findcard2s  6866  fiintim  6904  prnmaddl  7445  0re  7913  cnegexlem2  8088  0cnALT  8102  bndndx  9127  uzn0  9495  ublbneg  9565  rexanuz2  10948  opnneiid  12923  2sqlem2  13710  bj-inf2vnlem2  13971
  Copyright terms: Public domain W3C validator