| 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 4782 | . . 3 ⊢ ({𝐴} ⊆ 𝐵 ↔ (𝐴 ∈ V → 𝐴 ∈ 𝐵)) | |
| 2 | 1 | bicomi 224 | . 2 ⊢ ((𝐴 ∈ V → 𝐴 ∈ 𝐵) ↔ {𝐴} ⊆ 𝐵) |
| 3 | elex 3501 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
| 4 | imbibi 391 | . 2 ⊢ (((𝐴 ∈ V → 𝐴 ∈ 𝐵) ↔ {𝐴} ⊆ 𝐵) → (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))) | |
| 5 | 2, 3, 4 | mpsyl 68 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∈ wcel 2108 Vcvv 3480 ⊆ wss 3951 {csn 4626 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-sn 4627 |
| This theorem is referenced by: snss 4785 tppreqb 4805 snssi 4808 prssg 4819 snelpwg 5447 relsng 5811 fvimacnvALT 7077 fr3nr 7792 vdwapid1 17013 acsfn 17702 cycsubg2 19228 cycsubg2cl 19229 pgpfac1lem1 20094 pgpfac1lem3a 20096 pgpfac1lem3 20097 pgpfac1lem5 20099 pgpfaclem2 20102 lspsnid 20991 lidldvgen 21344 isneip 23113 elnei 23119 iscnp4 23271 cnpnei 23272 nlly2i 23484 1stckgenlem 23561 flimopn 23983 flimclslem 23992 fclsneii 24025 fcfnei 24043 rrx0el 25432 limcvallem 25906 ellimc2 25912 limcflf 25916 limccnp 25926 limccnp2 25927 limcco 25928 lhop2 26054 plyrem 26347 isppw 27157 lpvtx 29085 h1did 31570 rspsnid 33399 dvdsrspss 33415 unitpidl1 33452 mxidlirred 33500 qsdrngilem 33522 evls1fldgencl 33720 erdszelem8 35203 neibastop2 36362 prnc 38074 proot1mul 43206 uneqsn 44038 mnuprdlem1 44291 islptre 45634 rrxsnicc 46315 sclnbgrelself 47834 |
| Copyright terms: Public domain | W3C validator |