Theorem snssg 4740

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 4739	. . 3 ⊢ ({𝐴} ⊆ 𝐵 ↔ (𝐴 ∈ V → 𝐴 ∈ 𝐵))
2	1	bicomi 224	. 2 ⊢ ((𝐴 ∈ V → 𝐴 ∈ 𝐵) ↔ {𝐴} ⊆ 𝐵)
3		elex 3461	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
4		imbibi 391	. 2 ⊢ (((𝐴 ∈ V → 𝐴 ∈ 𝐵) ↔ {𝐴} ⊆ 𝐵) → (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)))
5	2, 3, 4	mpsyl 68	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2113  Vcvv 3440   ⊆ wss 3901  {csn 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-sn 4581

This theorem is referenced by:  snss  4741  tppreqb  4761  snssi  4764  prssg  4775  snelpwg  5391  relsng  5750  fvimacnvALT  7002  fr3nr  7717  vdwapid1  16903  acsfn  17582  cycsubg2  19139  cycsubg2cl  19140  pgpfac1lem1  20005  pgpfac1lem3a  20007  pgpfac1lem3  20008  pgpfac1lem5  20010  pgpfaclem2  20013  lspsnid  20944  lidldvgen  21289  isneip  23049  elnei  23055  iscnp4  23207  cnpnei  23208  nlly2i  23420  1stckgenlem  23497  flimopn  23919  flimclslem  23928  fclsneii  23961  fcfnei  23979  rrx0el  25354  limcvallem  25828  ellimc2  25834  limcflf  25838  limccnp  25848  limccnp2  25849  limcco  25850  lhop2  25976  plyrem  26269  isppw  27080  lpvtx  29141  h1did  31626  prssad  32604  prssbd  32605  tpssg  32612  rspsnid  33452  dvdsrspss  33468  unitpidl1  33505  mxidlirred  33553  qsdrngilem  33575  evls1fldgencl  33827  erdszelem8  35392  neibastop2  36555  prnc  38264  proot1mul  43432  uneqsn  44262  mnuprdlem1  44509  islptre  45861  rrxsnicc  46540  sclnbgrelself  48090