Theorem ssequn1 2171

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 2021	. . 3 |- (A u. B) = {x | (x e. A \/ x e. B)}
2	1	eqeq2i 1461	. 2 |- (B = (A u. B) <-> B = {x | (x e. A \/ x e. B)})
3		eqcom 1453	. 2 |- ((A u. B) = B <-> B = (A u. B))
4		pm4.72 639	. . . 4 |- ((x e. A -> x e. B) <-> (x e. B <-> (x e. A \/ x e. B)))
5	4	albii 975	. . 3 |- (A.x(x e. A -> x e. B) <-> A.x(x e. B <-> (x e. A \/ x e. B)))
6		dfss2 2029	. . 3 |- (A (_ B <-> A.x(x e. A -> x e. B))
7		abeq2 1544	. . 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 950   = wceq 1099   e. wcel 1105  {cab 1440   u. cun 2016   (_ wss 2018

This theorem is referenced by:  ssequn2 2174  undif 2314  uniop 2771  pwssun 2789  unisuc 3009  ordssun 3042  ordequn 3043  onuninsuc 3071  onun 3073  oaabs 4190  rankop 4617  ranksuc 4624  kmlem11 4699

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-clab 1441  df-cleq 1446  df-clel 1449  df-un 2021  df-in 2022  df-ss 2024

Copyright terms: Public domain