Theorem snssg 4451

Description: The singleton of an element of a class is a subset of the class (general form of snss 4452). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.)

Assertion

Ref	Expression
snssg	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))

Proof of Theorem snssg

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		velsn 4333	. . . . 5 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	imbi1i 338	. . . 4 ⊢ ((𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3	2	albii 1895	. . 3 ⊢ (∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
4	3	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)))
5		dfss2 3740	. . 3 ⊢ ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵))
6	5	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵)))
7		clel2g 3489	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)))
8	4, 6, 7	3bitr4rd 301	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1629   = wceq 1631   ∈ wcel 2145   ⊆ wss 3723  {csn 4317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-in 3730  df-ss 3737  df-sn 4318

This theorem is referenced by:  snss  4452  tppreqb  4472  snssi  4475  prssg  4486  relsng  5362  fvimacnvALT  6481  fr3nr  7130  vdwapid1  15886  acsfn  16527  cycsubg2  17839  cycsubg2cl  17840  pgpfac1lem1  18681  pgpfac1lem3a  18683  pgpfac1lem3  18684  pgpfac1lem5  18686  pgpfaclem2  18689  lspsnid  19206  lidldvgen  19470  isneip  21130  elnei  21136  iscnp4  21288  cnpnei  21289  nlly2i  21500  1stckgenlem  21577  flimopn  21999  flimclslem  22008  fclsneii  22041  fcfnei  22059  limcvallem  23855  ellimc2  23861  limcflf  23865  limccnp  23875  limccnp2  23876  limcco  23877  lhop2  23998  plyrem  24280  isppw  25061  lpvtx  26184  h1did  28750  erdszelem8  31518  neibastop2  32693  prnc  34196  proot1mul  38301  uneqsn  38845  islptre  40364  rrxsnicc  41032