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

Theorem rexlimivw 2429
 Description: Weaker version of rexlimiv 2427. (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 2427 1 (∃𝑥𝐴 𝜑𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∈ wcel 1393  ∃wrex 2307 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-i5r 1428 This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311  df-rex 2312 This theorem is referenced by:  r19.29vva  2456  eliun  3661  reusv3i  4191  elrnmptg  4586  fun11iun  5147  fmpt  5319  fliftfun  5436  elrnmpt2  5614  releldm2  5811  tfrlem4  5929  iinerm  6178  isfi  6241  cardcl  6361  cardval3ex  6365  ltbtwnnqq  6513  recexprlemlol  6724  recexprlemupu  6726
 Copyright terms: Public domain W3C validator