![]() |
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 4625). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.) |
Ref | Expression |
---|---|
snssg | ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | velsn 4488 | . . . . 5 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | |
2 | 1 | imbi1i 351 | . . . 4 ⊢ ((𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ (𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) |
3 | 2 | albii 1801 | . . 3 ⊢ (∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) |
4 | 3 | a1i 11 | . 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))) |
5 | dfss2 3877 | . . 3 ⊢ ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵)) | |
6 | 5 | a1i 11 | . 2 ⊢ (𝐴 ∈ 𝑉 → ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵))) |
7 | clel2g 3590 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))) | |
8 | 4, 6, 7 | 3bitr4rd 313 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∀wal 1520 = wceq 1522 ∈ wcel 2081 ⊆ wss 3859 {csn 4472 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-v 3439 df-in 3866 df-ss 3874 df-sn 4473 |
This theorem is referenced by: snss 4625 tppreqb 4645 snssi 4648 prssg 4659 relsng 5560 fvimacnvALT 6692 fr3nr 7350 vdwapid1 16140 acsfn 16759 cycsubg2 18070 cycsubg2cl 18071 pgpfac1lem1 18913 pgpfac1lem3a 18915 pgpfac1lem3 18916 pgpfac1lem5 18918 pgpfaclem2 18921 lspsnid 19455 lidldvgen 19717 isneip 21397 elnei 21403 iscnp4 21555 cnpnei 21556 nlly2i 21768 1stckgenlem 21845 flimopn 22267 flimclslem 22276 fclsneii 22309 fcfnei 22327 rrx0el 23684 limcvallem 24152 ellimc2 24158 limcflf 24162 limccnp 24172 limccnp2 24173 limcco 24174 lhop2 24295 plyrem 24577 isppw 25373 lpvtx 26536 h1did 29019 erdszelem8 32053 neibastop2 33318 prnc 34877 proot1mul 39284 uneqsn 39858 mnuprdlem1 40105 islptre 41442 rrxsnicc 42127 |
Copyright terms: Public domain | W3C validator |