Theorem snssg 4624

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.)

Assertion

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

Proof of Theorem snssg

Dummy variable 𝑥 is distinct from all other variables.

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 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))

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