![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > snssg | Structured version Visualization version GIF version |
Description: The singleton formed on a set is included in a class if and only if the set is an element of that class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.) (Proof shortened by BJ, 1-Jan-2025.) |
Ref | Expression |
---|---|
snssg | ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snssb 4788 | . . 3 ⊢ ({𝐴} ⊆ 𝐵 ↔ (𝐴 ∈ V → 𝐴 ∈ 𝐵)) | |
2 | 1 | bicomi 223 | . 2 ⊢ ((𝐴 ∈ V → 𝐴 ∈ 𝐵) ↔ {𝐴} ⊆ 𝐵) |
3 | elex 3480 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
4 | imbibi 390 | . 2 ⊢ (((𝐴 ∈ V → 𝐴 ∈ 𝐵) ↔ {𝐴} ⊆ 𝐵) → (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))) | |
5 | 2, 3, 4 | mpsyl 68 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∈ wcel 2098 Vcvv 3461 ⊆ wss 3944 {csn 4630 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-v 3463 df-ss 3961 df-sn 4631 |
This theorem is referenced by: snss 4791 tppreqb 4810 snssi 4813 prssg 4824 snelpwg 5444 relsng 5803 fvimacnvALT 7065 fr3nr 7775 vdwapid1 16947 acsfn 17642 cycsubg2 19173 cycsubg2cl 19174 pgpfac1lem1 20043 pgpfac1lem3a 20045 pgpfac1lem3 20046 pgpfac1lem5 20048 pgpfaclem2 20051 lspsnid 20889 lidldvgen 21241 isneip 23053 elnei 23059 iscnp4 23211 cnpnei 23212 nlly2i 23424 1stckgenlem 23501 flimopn 23923 flimclslem 23932 fclsneii 23965 fcfnei 23983 rrx0el 25370 limcvallem 25844 ellimc2 25850 limcflf 25854 limccnp 25864 limccnp2 25865 limcco 25866 lhop2 25992 plyrem 26285 isppw 27091 lpvtx 28953 h1did 31433 rspsnid 33183 dvdsrspss 33199 unitpidl1 33236 mxidlirred 33284 qsdrngilem 33306 evls1fldgencl 33489 erdszelem8 34939 neibastop2 35976 prnc 37671 proot1mul 42764 uneqsn 43597 mnuprdlem1 43851 islptre 45145 rrxsnicc 45826 sclnbgrelself 47320 |
Copyright terms: Public domain | W3C validator |