Theorem elpwi 2404

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 2403	. 2 |- (A e. P~B -> (A e. P~B <-> A (_ B))
2	1	ibi 591	1 |- (A e. P~B -> A (_ B)

Syntax hints:   -> wi 3   e. wcel 957   (_ wss 2045  P~cpw 2399

This theorem is referenced by:  elpw2g 2724  eldifpw 2907  elpwunsn 2909  iunpw 2911  acdc3lem 7464  acdc2lem1 7466  acdc5lem1 7469  acdclem 7472  islp2 7726  bcthlem28 8009  bcthlem30 8011  bcthlem33 8014  inpws1 10444  iooirrsa 10473  fgsb 10538  fgsb2 10543

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1810  df-in 2049  df-ss 2051  df-pw 2400

Copyright terms: Public domain