![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iotaex | Structured version Visualization version GIF version |
Description: Theorem 8.23 in [Quine] p. 58. This theorem proves the existence of the ℩ class under our definition. (Contributed by Andrew Salmon, 11-Jul-2011.) Remove dependency on ax-10 2130, ax-11 2147, ax-12 2167. (Revised by SN, 6-Nov-2024.) |
Ref | Expression |
---|---|
iotaex | ⊢ (℩𝑥𝜑) ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iotaval2 6516 | . . . 4 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = 𝑦) | |
2 | vex 3475 | . . . 4 ⊢ 𝑦 ∈ V | |
3 | 1, 2 | eqeltrdi 2837 | . . 3 ⊢ ({𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V) |
4 | 3 | exlimiv 1926 | . 2 ⊢ (∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V) |
5 | iotanul2 6518 | . . 3 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) = ∅) | |
6 | 0ex 5307 | . . 3 ⊢ ∅ ∈ V | |
7 | 5, 6 | eqeltrdi 2837 | . 2 ⊢ (¬ ∃𝑦{𝑥 ∣ 𝜑} = {𝑦} → (℩𝑥𝜑) ∈ V) |
8 | 4, 7 | pm2.61i 182 | 1 ⊢ (℩𝑥𝜑) ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1534 ∃wex 1774 ∈ wcel 2099 {cab 2705 Vcvv 3471 ∅c0 4323 {csn 4629 ℩cio 6498 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-nul 5306 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ne 2938 df-v 3473 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4324 df-sn 4630 df-pr 4632 df-uni 4909 df-iota 6500 |
This theorem is referenced by: iota4an 6530 fvex 6910 riotaex 7380 erov 8833 iunfictbso 10138 isf32lem9 10385 sumex 15667 prodex 15884 pcval 16813 grpidval 18621 fn0g 18623 gsumvalx 18636 psgnfn 19456 psgnval 19462 dchrptlem1 27210 lgsdchrval 27300 lgsdchr 27301 nosupno 27649 nosupdm 27650 nosupbday 27651 nosupfv 27652 nosupres 27653 nosupbnd1lem1 27654 noinfno 27664 noinfdm 27665 noinffv 27667 bnj1366 34460 bj-finsumval0 36764 ellimciota 45002 fourierdlem36 45531 eubrdm 46418 dfatafv2ex 46593 afv2ex 46594 funressndmafv2rn 46603 |
Copyright terms: Public domain | W3C validator |