Theorem ssequn1 2200

Description: A relationship between subclass and union. Theorem 26 of [Suppes] p. 27.

Assertion

Ref	Expression
ssequn1	|- (A (_ B <-> (A u. B) = B)

Proof of Theorem ssequn1

Step	Hyp	Ref	Expression
1		df-un 2050	. . 3 |- (A u. B) = {x | (x e. A \/ x e. B)}
2	1	eqeq2i 1485	. 2 |- (B = (A u. B) <-> B = {x | (x e. A \/ x e. B)})
3		eqcom 1477	. 2 |- ((A u. B) = B <-> B = (A u. B))
4		pm4.72 641	. . . 4 |- ((x e. A -> x e. B) <-> (x e. B <-> (x e. A \/ x e. B)))
5	4	albii 999	. . 3 |- (A.x(x e. A -> x e. B) <-> A.x(x e. B <-> (x e. A \/ x e. B)))
6		dfss2 2058	. . 3 |- (A (_ B <-> A.x(x e. A -> x e. B))
7		abeq2 1568	. . 3 |- (B = {x | (x e. A \/ x e. B)} <-> A.x(x e. B <-> (x e. A \/ x e. B)))
8	5, 6, 7	3bitr4 183	. 2 |- (A (_ B <-> B = {x | (x e. A \/ x e. B)})
9	2, 3, 8	3bitr4r 184	1 |- (A (_ B <-> (A u. B) = B)

Syntax hints:   -> wi 3   <-> wb 146   \/ wo 222  A.wal 954   = wceq 956   e. wcel 958  {cab 1463   u. cun 2045   (_ wss 2047

This theorem is referenced by:  ssequn2 2203  undif 2343  uniop 2808  pwssun 2827  unisuc 3046  ordssun 3079  ordequn 3080  onuninsuc 3108  onun 3110  oaabs 4252  rankop 4693  ranksuc 4700  kmlem11 4775

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-un 2050  df-in 2051  df-ss 2053

Copyright terms: Public domain