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

Theorem rexlimiv 2588
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 1528 . 2  |-  F/ x ps
2 rexlimiv.1 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
31, 2rexlimi 2587 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 2148   E.wrex 2456
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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461
This theorem is referenced by:  rexlimiva  2589  rexlimivw  2590  rexlimivv  2600  r19.36av  2628  r19.44av  2636  r19.45av  2637  rexn0  3522  uniss2  3841  elres  4944  ssimaex  5578  mpoexw  6214  tfrlem5  6315  tfrlem8  6319  ecoptocl  6622  mapsn  6690  elixpsn  6735  ixpsnf1o  6736  findcard  6888  findcard2  6889  findcard2s  6890  fiintim  6928  prnmaddl  7489  0re  7957  cnegexlem2  8133  0cnALT  8147  bndndx  9175  uzn0  9543  ublbneg  9613  rexanuz2  11000  opnneiid  13667  2sqlem2  14465  bj-inf2vnlem2  14726
  Copyright terms: Public domain W3C validator