Theorem snssg 4739

Description: The singleton formed on a set is included in a class if and only if the set is an element of that class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.) (Proof shortened by BJ, 1-Jan-2025.)

Assertion

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

Proof of Theorem snssg

Step	Hyp	Ref	Expression
1		snssb 4738	. . 3 ⊢ ({𝐴} ⊆ 𝐵 ↔ (𝐴 ∈ V → 𝐴 ∈ 𝐵))
2	1	bicomi 226	. 2 ⊢ ((𝐴 ∈ V → 𝐴 ∈ 𝐵) ↔ {𝐴} ⊆ 𝐵)
3		elex 3474	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
4		imbibi 394	. 2 ⊢ (((𝐴 ∈ V → 𝐴 ∈ 𝐵) ↔ {𝐴} ⊆ 𝐵) → (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)))
5	2, 3, 4	mpsyl 68	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2141  Vcvv 3453   ⊆ wss 3902  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3919  df-sn 4580

This theorem is referenced by:  snss  4740  snssi  4741  tppreqb  4762  prssg  4774  snelpwg  5407  relsng  5770  fvimacnvALT  7032  fr3nr  7749  sucprcreg  9547  vdwapid1  17001  acsfn  17681  cycsubg2  19241  cycsubg2cl  19242  pgpfac1lem1  20106  pgpfac1lem3a  20108  pgpfac1lem3  20109  pgpfac1lem5  20111  pgpfaclem2  20114  lspsnid  21047  lidldvgen  21391  isneip  23152  elnei  23158  iscnp4  23310  cnpnei  23311  nlly2i  23523  1stckgenlem  23600  flimopn  24022  flimclslem  24031  fclsneii  24064  fcfnei  24082  rrx0el  25447  limcvallem  25920  ellimc2  25926  limcflf  25930  limccnp  25940  limccnp2  25941  limcco  25942  lhop2  26064  plyrem  26356  isppw  27165  lpvtx  29225  h1did  31710  prssad  32687  prssbd  32688  tpssg  32695  rspsnid  33517  dvdsrspss  33533  unitpidl1  33570  mxidlirred  33620  qsdrngilem  33642  evls1fldgencl  33927  erdszelem8  35508  neibastop2  36681  prnc  38526  proot1mul  43731  uneqsn  44561  mnuprdlem1  44808  islptre  46155  rrxsnicc  46834  sclnbgrelself  48430