Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > snssg | Structured version Visualization version GIF version |
Description: The singleton of an element of a class is a subset of the class (general form of snss 4710). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.) |
Ref | Expression |
---|---|
snssg | ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | velsn 4573 | . . . . 5 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | |
2 | 1 | imbi1i 351 | . . . 4 ⊢ ((𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ (𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) |
3 | 2 | albii 1811 | . . 3 ⊢ (∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) |
4 | 3 | a1i 11 | . 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))) |
5 | dfss2 3952 | . . 3 ⊢ ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵)) | |
6 | 5 | a1i 11 | . 2 ⊢ (𝐴 ∈ 𝑉 → ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵))) |
7 | clel2g 3649 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))) | |
8 | 4, 6, 7 | 3bitr4rd 313 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∀wal 1526 = wceq 1528 ∈ wcel 2105 ⊆ wss 3933 {csn 4557 |
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-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-in 3940 df-ss 3949 df-sn 4558 |
This theorem is referenced by: snss 4710 tppreqb 4730 snssi 4733 prssg 4744 relsng 5667 fvimacnvALT 6819 fr3nr 7483 vdwapid1 16299 acsfn 16918 cycsubg2 18291 cycsubg2cl 18292 pgpfac1lem1 19125 pgpfac1lem3a 19127 pgpfac1lem3 19128 pgpfac1lem5 19130 pgpfaclem2 19133 lspsnid 19694 lidldvgen 19956 isneip 21641 elnei 21647 iscnp4 21799 cnpnei 21800 nlly2i 22012 1stckgenlem 22089 flimopn 22511 flimclslem 22520 fclsneii 22553 fcfnei 22571 rrx0el 23928 limcvallem 24396 ellimc2 24402 limcflf 24406 limccnp 24416 limccnp2 24417 limcco 24418 lhop2 24539 plyrem 24821 isppw 25618 lpvtx 26780 h1did 29255 rspsnid 30864 erdszelem8 32342 neibastop2 33606 prnc 35226 proot1mul 39677 uneqsn 40251 mnuprdlem1 40485 islptre 41776 rrxsnicc 42462 |
Copyright terms: Public domain | W3C validator |