Theorem unss 2256

Description: The union of two subclasses is a subclass. Theorem 27 of [Suppes] p. 27 and its converse.

Assertion

Ref	Expression
unss	⊢ ((A ⊆ C ⋀ B ⊆ C) ↔ (A ∪ B) ⊆ C)

Proof of Theorem unss

Step	Hyp	Ref	Expression
1		elun 2225	. . . . 5 ⊢ (x ∈ (A ∪ B) ↔ (x ∈ A ⋁ x ∈ B))
2	1	imbi1i 184	. . . 4 ⊢ ((x ∈ (A ∪ B) → x ∈ C) ↔ ((x ∈ A ⋁ x ∈ B) → x ∈ C))
3		jaob 422	. . . 4 ⊢ (((x ∈ A ⋁ x ∈ B) → x ∈ C) ↔ ((x ∈ A → x ∈ C) ⋀ (x ∈ B → x ∈ C)))
4	2, 3	bitri 171	. . 3 ⊢ ((x ∈ (A ∪ B) → x ∈ C) ↔ ((x ∈ A → x ∈ C) ⋀ (x ∈ B → x ∈ C)))
5	4	albii 1035	. 2 ⊢ (∀x(x ∈ (A ∪ B) → x ∈ C) ↔ ∀x((x ∈ A → x ∈ C) ⋀ (x ∈ B → x ∈ C)))
6		dfss2 2110	. 2 ⊢ ((A ∪ B) ⊆ C ↔ ∀x(x ∈ (A ∪ B) → x ∈ C))
7		dfss2 2110	. . . 4 ⊢ (A ⊆ C ↔ ∀x(x ∈ A → x ∈ C))
8		dfss2 2110	. . . 4 ⊢ (B ⊆ C ↔ ∀x(x ∈ B → x ∈ C))
9	7, 8	anbi12i 485	. . 3 ⊢ ((A ⊆ C ⋀ B ⊆ C) ↔ (∀x(x ∈ A → x ∈ C) ⋀ ∀x(x ∈ B → x ∈ C)))
10		19.26 1103	. . 3 ⊢ (∀x((x ∈ A → x ∈ C) ⋀ (x ∈ B → x ∈ C)) ↔ (∀x(x ∈ A → x ∈ C) ⋀ ∀x(x ∈ B → x ∈ C)))
11	9, 10	bitr4i 174	. 2 ⊢ ((A ⊆ C ⋀ B ⊆ C) ↔ ∀x((x ∈ A → x ∈ C) ⋀ (x ∈ B → x ∈ C)))
12	5, 6, 11	3bitr4ri 182	1 ⊢ ((A ⊆ C ⋀ B ⊆ C) ↔ (A ∪ B) ⊆ C)

Syntax hints:   → wi 3   ↔ wb 144   ⋁ wo 220   ⋀ wa 221  ∀wal 990   ∈ wcel 994   ∪ cun 2097   ⊆ wss 2099

This theorem is referenced by:  unssi 2257  nsspssun 2293  uneqin 2308  eldifpw 3133  suceloni 3170  ordunel 3181  eqrelrel 3341  xpsspw 3346  relun 3350  dfer2 4402  abfii4 4707  trcl 4791  supxrun 6253  infxpidmlem11 7774  subbas 7856  uncld 7891  clslp 7958  dfchj2 9600  sshjcl 9603  shlubi 9622  spanuni 9743  infi1 10735  ficli 10756  twpar2 10773  infi 10854  toplat 10884  cnfilca 11088  rcfpfillem4 11092  finsschain 11425  clsun 11465  subntr 11482  cptclsscpt 11489  uncomp 11490  alexsublem3 11498  alexsublem4 11499  comppfsc 11578  extbas2 11642  ufprim 11654  ufcondr 11666  fmfnfm 11704  indexf 11847

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-un 2102  df-in 2103  df-ss 2105

Copyright terms: Public domain