Theorem elpwi 2458

Description: Subset relation implied by membership in a power class.

Assertion

Ref	Expression
elpwi	|- (A e. P~B -> A (_ B)

Proof of Theorem elpwi

Step	Hyp	Ref	Expression
1		elpwg 2457	. 2 |- (A e. P~B -> (A e. P~B <-> A (_ B))
2	1	ibi 603	1 |- (A e. P~B -> A (_ B)

Syntax hints:   -> wi 3   e. wcel 999   (_ wss 2098  P~cpw 2453

This theorem is referenced by:  elpw2g 2782  eldifpw 2967  elpwunsn 2969  iunpw 2971  acdc3lem 7578  acdc2lem1 7580  acdc5lem1 7583  acdclem 7586  islp2 7832  bcthlem28 8111  bcthlem30 8113  bcthlem33 8116  inpws1 10536  iooirrsa 10586  fgsb 10663  fgsb2 10668

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-12 1009  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022  df-sb 1214  df-clab 1510  df-cleq 1515  df-clel 1518  df-v 1859  df-in 2102  df-ss 2104  df-pw 2454

Copyright terms: Public domain