Theorem ssequn1 2196

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

Assertion

Ref	Expression
ssequn1	⊢ (A ⊆ B ↔ (A ∪ B) = B)

Proof of Theorem ssequn1

Step	Hyp	Ref	Expression
1		df-un 2046	. . 3 ⊢ (A ∪ B) = {x∣(x ∈ A ⋁ x ∈ B)}
2	1	eqeq2i 1482	. 2 ⊢ (B = (A ∪ B) ↔ B = {x∣(x ∈ A ⋁ x ∈ B)})
3		eqcom 1474	. 2 ⊢ ((A ∪ B) = B ↔ B = (A ∪ B))
4		pm4.72 640	. . . 4 ⊢ ((x ∈ A → x ∈ B) ↔ (x ∈ B ↔ (x ∈ A ⋁ x ∈ B)))
5	4	albii 997	. . 3 ⊢ (∀x(x ∈ A → x ∈ B) ↔ ∀x(x ∈ B ↔ (x ∈ A ⋁ x ∈ B)))
6		dfss2 2054	. . 3 ⊢ (A ⊆ B ↔ ∀x(x ∈ A → x ∈ B))
7		abeq2 1565	. . 3 ⊢ (B = {x∣(x ∈ A ⋁ x ∈ B)} ↔ ∀x(x ∈ B ↔ (x ∈ A ⋁ x ∈ B)))
8	5, 6, 7	3bitr4 183	. 2 ⊢ (A ⊆ B ↔ B = {x∣(x ∈ A ⋁ x ∈ B)})
9	2, 3, 8	3bitr4r 184	1 ⊢ (A ⊆ B ↔ (A ∪ B) = B)

Syntax hints:   → wi 3   ↔ wb 146   ⋁ wo 222  ∀wal 952   = wceq 954   ∈ wcel 956  {cab 1461   ∪ cun 2041   ⊆ wss 2043

This theorem is referenced by:  ssequn2 2199  undif 2339  uniop 2803  pwssun 2822  unisuc 3041  ordssun 3074  ordequn 3075  onuninsuc 3103  onun 3105  oaabs 4242  rankop 4673  ranksuc 4680  kmlem11 4755

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-un 2046  df-in 2047  df-ss 2049

Copyright terms: Public domain