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

Theorem rexlimiv 2472
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 20-Nov-1994.)
Hypothesis
Ref Expression
rexlimiv.1  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
Assertion
Ref Expression
rexlimiv  |-  ( E. x  e.  A  ph  ->  ps )
Distinct variable group:    ps, x
Allowed substitution hints:    ph( x)    A( x)

Proof of Theorem rexlimiv
StepHypRef Expression
1 nfv 1462 . 2  |-  F/ x ps
2 rexlimiv.1 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
31, 2rexlimi 2471 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1434   E.wrex 2350
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-i5r 1469
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-ral 2354  df-rex 2355
This theorem is referenced by:  rexlimiva  2473  rexlimivw  2474  rexlimivv  2483  r19.36av  2506  r19.44av  2514  r19.45av  2515  rexn0  3347  uniss2  3640  elres  4674  ssimaex  5266  tfrlem5  5963  tfrlem8  5967  ecoptocl  6259  findcard  6422  findcard2  6423  findcard2s  6424  prnmaddl  6742  0re  7181  cnegexlem2  7351  0cnALT  7365  bndndx  8354  uzn0  8715  ublbneg  8779  rexanuz2  10015  bj-inf2vnlem2  10924
  Copyright terms: Public domain W3C validator