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

Theorem rexlimivw 2479
Description: Weaker version of rexlimiv 2477. (Contributed by FL, 19-Sep-2011.)
Hypothesis
Ref Expression
rexlimivw.1 (𝜑𝜓)
Assertion
Ref Expression
rexlimivw (∃𝑥𝐴 𝜑𝜓)
Distinct variable group:   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimivw
StepHypRef Expression
1 rexlimivw.1 . . 3 (𝜑𝜓)
21a1i 9 . 2 (𝑥𝐴 → (𝜑𝜓))
32rexlimiv 2477 1 (∃𝑥𝐴 𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1434  wrex 2354
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 2358  df-rex 2359
This theorem is referenced by:  r19.29vva  2506  eliun  3708  reusv3i  4245  elrnmptg  4645  fun11iun  5222  fmpt  5394  fliftfun  5515  elrnmpt2  5693  releldm2  5890  tfrlem4  6010  iinerm  6294  isfi  6408  cardcl  6712  cardval3ex  6716  ltbtwnnqq  6877  recexprlemlol  7088  recexprlemupu  7090
  Copyright terms: Public domain W3C validator