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

Theorem rexlimivw 2545
 Description: Weaker version of rexlimiv 2543. (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 2543 1 (∃𝑥𝐴 𝜑𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∈ wcel 1480  ∃wrex 2417 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-i5r 1515 This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421  df-rex 2422 This theorem is referenced by:  r19.29vva  2577  eliun  3817  reusv3i  4380  elrnmptg  4791  fun11iun  5388  fmpt  5570  fliftfun  5697  elrnmpo  5884  releldm2  6083  tfrlem4  6210  iinerm  6501  elixpsn  6629  isfi  6655  cardcl  7042  cardval3ex  7046  ltbtwnnqq  7235  recexprlemlol  7446  recexprlemupu  7448  suplocsr  7629  restsspw  12144  ssnei  12334  tgcnp  12392  xmetunirn  12541  metss  12677  metrest  12689
 Copyright terms: Public domain W3C validator