Theorem snssg 4715

Description: The singleton of an element of a class is a subset of the class (general form of snss 4716). 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 4574	. . . . 5 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	imbi1i 349	. . . 4 ⊢ ((𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3	2	albii 1823	. . 3 ⊢ (∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
4	3	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)))
5		dfss2 3903	. . 3 ⊢ ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵))
6	5	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵)))
7		clel2g 3581	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)))
8	4, 6, 7	3bitr4rd 311	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1537   = wceq 1539   ∈ wcel 2108   ⊆ wss 3883  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-sn 4559

This theorem is referenced by:  snss  4716  tppreqb  4735  snssi  4738  prssg  4749  relsng  5700  fvimacnvALT  6916  fr3nr  7600  vdwapid1  16604  acsfn  17285  cycsubg2  18744  cycsubg2cl  18745  pgpfac1lem1  19592  pgpfac1lem3a  19594  pgpfac1lem3  19595  pgpfac1lem5  19597  pgpfaclem2  19600  lspsnid  20170  lidldvgen  20439  isneip  22164  elnei  22170  iscnp4  22322  cnpnei  22323  nlly2i  22535  1stckgenlem  22612  flimopn  23034  flimclslem  23043  fclsneii  23076  fcfnei  23094  rrx0el  24467  limcvallem  24940  ellimc2  24946  limcflf  24950  limccnp  24960  limccnp2  24961  limcco  24962  lhop2  25084  plyrem  25370  isppw  26168  lpvtx  27341  h1did  29814  rspsnid  31470  erdszelem8  33060  neibastop2  34477  prnc  36152  proot1mul  40940  uneqsn  41522  mnuprdlem1  41779  islptre  43050  rrxsnicc  43731