New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > rexlimivw | GIF version |
Description: Weaker version of rexlimiv 2732. (Contributed by FL, 19-Sep-2011.) |
Ref | Expression |
---|---|
rexlimivw.1 | ⊢ (φ → ψ) |
Ref | Expression |
---|---|
rexlimivw | ⊢ (∃x ∈ A φ → ψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimivw.1 | . . 3 ⊢ (φ → ψ) | |
2 | 1 | a1i 10 | . 2 ⊢ (x ∈ A → (φ → ψ)) |
3 | 2 | rexlimiv 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 |