NFE Home 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