Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rexlimi | Structured version Visualization version GIF version |
Description: Restricted quantifier version of exlimi 2207. (Contributed by NM, 30-Nov-2003.) (Proof shortened by Andrew Salmon, 30-May-2011.) |
Ref | Expression |
---|---|
rexlimi.1 | ⊢ Ⅎ𝑥𝜓 |
rexlimi.2 | ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) |
Ref | Expression |
---|---|
rexlimi | ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexlimi.2 | . . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓)) | |
2 | 1 | rgen 3145 | . 2 ⊢ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) |
3 | rexlimi.1 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
4 | 3 | r19.23 3311 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)) |
5 | 2, 4 | mpbi 231 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Ⅎwnf 1775 ∈ wcel 2105 ∀wral 3135 ∃wrex 3136 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-12 2167 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-nf 1776 df-ral 3140 df-rex 3141 |
This theorem is referenced by: reuan 3877 triun 5176 reusv1 5288 reusv3 5296 iunopeqop 5402 tfinds 7563 fiun 7633 f1iun 7634 iunfo 9949 iundom2g 9950 fsumcom2 15117 fprodcom2 15326 dfon2lem7 32931 nosupbnd1 33111 nosupbnd2 33113 finminlem 33563 r19.36vf 41280 allbutfiinf 41570 infxrunb3rnmpt 41578 hoidmvlelem1 42754 2zrngmmgm 44145 |
Copyright terms: Public domain | W3C validator |