Theorem snelpwi 5418

Description: If a set is a member of a class, then the singleton of that set is a member of the powerclass of that class. (Contributed by Alan Sare, 25-Aug-2011.)

Assertion

Ref	Expression
snelpwi	⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)

Proof of Theorem snelpwi

Step	Hyp	Ref	Expression
1		snelpwg 5417	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ 𝒫 𝐵))
2	1	ibi 267	1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2108  𝒫 cpw 4575  {csn 4601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943  df-pw 4577  df-sn 4602  df-pr 4604

This theorem is referenced by:  unipw  5425  canth2  9144  pwfir  9327  unifpw  9367  marypha1lem  9445  infpwfidom  10042  ackbij1lem4  10236  acsfn  17671  sylow2a  19600  dissnref  23466  dissnlocfin  23467  locfindis  23468  txdis  23570  txdis1cn  23573  symgtgp  24044  1sno  27791  bday0s  27792  bday0b  27794  bday1s  27795  cutneg  27797  cutlt  27892  onscutlt  28217  n0sbday  28296  n0sfincut  28298  bdayn0p1  28310  zscut  28347  1p1e2s  28354  twocut  28361  addhalfcut  28386  dispcmp  33890  esumcst  34094  cntnevol  34259  coinflippvt  34517  onsucsuccmpi  36461  topdifinffinlem  37365  pclfinN  39919  lpirlnr  43141  unipwrVD  44856  unipwr  44857  salexct  46363  salexct3  46371  salgencntex  46372  salgensscntex  46373  sge0tsms  46409  sge0cl  46410  sge0sup  46420  isgrtri  47955  lincvalsng  48392  snlindsntor  48447