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

Theorem rexlimivw 2474
Description: Weaker version of rexlimiv 2472. (Contributed by FL, 19-Sep-2011.)
Hypothesis
Ref Expression
rexlimivw.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
rexlimivw  |-  ( E. x  e.  A  ph  ->  ps )
Distinct variable group:    ps, x
Allowed substitution hints:    ph( x)    A( x)

Proof of Theorem rexlimivw
StepHypRef Expression
1 rexlimivw.1 . . 3  |-  ( ph  ->  ps )
21a1i 9 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32rexlimiv 2472 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:  r19.29vva  2501  eliun  3690  reusv3i  4217  elrnmptg  4614  fun11iun  5178  fmpt  5351  fliftfun  5467  elrnmpt2  5645  releldm2  5842  tfrlem4  5962  iinerm  6244  isfi  6308  cardcl  6509  cardval3ex  6513  ltbtwnnqq  6667  recexprlemlol  6878  recexprlemupu  6880
  Copyright terms: Public domain W3C validator