New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  rexlimivw GIF version

Theorem rexlimivw 2734
 Description: Weaker version of rexlimiv 2732. (Contributed by FL, 19-Sep-2011.)
Hypothesis
Ref Expression
rexlimivw.1 (φψ)
Assertion
Ref Expression
rexlimivw (x A φψ)
Distinct variable group:   ψ,x
Allowed substitution hints:   φ(x)   A(x)

Proof of Theorem rexlimivw
StepHypRef Expression
1 rexlimivw.1 . . 3 (φψ)
21a1i 10 . 2 (x A → (φψ))
32rexlimiv 2732 1 (x A φψ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 1710  ∃wrex 2615 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545  df-ral 2619  df-rex 2620 This theorem is referenced by:  eliun  3973  eladdc  4398  tfinnnul  4490  phialllem1  4616  elima  4754  fun11iun  5305  fvelrnb  5365  fvelimab  5370  xpnedisj  5513  1st2nd2  5516  ovelrn  5608  fmpt  5692  enpw1  6062  eqtc  6161  addlec  6208  addceq0  6219  taddc  6229  nchoicelem14  6302  scancan  6331
 Copyright terms: Public domain W3C validator