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 4699). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.) |
Ref | Expression |
---|---|
snssg | ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | velsn 4557 | . . . . 5 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | |
2 | 1 | imbi1i 353 | . . . 4 ⊢ ((𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ (𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) |
3 | 2 | albii 1827 | . . 3 ⊢ (∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)) |
4 | 3 | a1i 11 | . 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))) |
5 | dfss2 3886 | . . 3 ⊢ ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵)) | |
6 | 5 | a1i 11 | . 2 ⊢ (𝐴 ∈ 𝑉 → ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵))) |
7 | clel2g 3566 | . 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))) | |
8 | 4, 6, 7 | 3bitr4rd 315 | 1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∀wal 1541 = wceq 1543 ∈ wcel 2110 ⊆ wss 3866 {csn 4541 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3410 df-in 3873 df-ss 3883 df-sn 4542 |
This theorem is referenced by: snss 4699 tppreqb 4718 snssi 4721 prssg 4732 relsng 5671 fvimacnvALT 6877 fr3nr 7557 vdwapid1 16528 acsfn 17162 cycsubg2 18617 cycsubg2cl 18618 pgpfac1lem1 19461 pgpfac1lem3a 19463 pgpfac1lem3 19464 pgpfac1lem5 19466 pgpfaclem2 19469 lspsnid 20030 lidldvgen 20293 isneip 22002 elnei 22008 iscnp4 22160 cnpnei 22161 nlly2i 22373 1stckgenlem 22450 flimopn 22872 flimclslem 22881 fclsneii 22914 fcfnei 22932 rrx0el 24295 limcvallem 24768 ellimc2 24774 limcflf 24778 limccnp 24788 limccnp2 24789 limcco 24790 lhop2 24912 plyrem 25198 isppw 25996 lpvtx 27159 h1did 29632 rspsnid 31282 erdszelem8 32873 neibastop2 34287 prnc 35962 proot1mul 40727 uneqsn 41310 mnuprdlem1 41563 islptre 42835 rrxsnicc 43516 |
Copyright terms: Public domain | W3C validator |