![]() |
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 2215. (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 3116 | . 2 ⊢ ∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) |
3 | rexlimi.1 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
4 | 3 | r19.23 3273 | . 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 → 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)) |
5 | 2, 4 | mpbi 233 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Ⅎwnf 1785 ∈ wcel 2111 ∀wral 3106 ∃wrex 3107 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-12 2175 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-nf 1786 df-ral 3111 df-rex 3112 |
This theorem is referenced by: reuan 3825 triun 5149 reusv1 5263 reusv3 5271 iunopeqop 5376 tfinds 7554 fiun 7626 f1iun 7627 iunfo 9950 iundom2g 9951 fsumcom2 15121 fprodcom2 15330 dfon2lem7 33147 nosupbnd1 33327 nosupbnd2 33329 finminlem 33779 r19.36vf 41772 allbutfiinf 42057 infxrunb3rnmpt 42065 hoidmvlelem1 43234 2zrngmmgm 44570 |
Copyright terms: Public domain | W3C validator |