Theorem unss 4138

Description: The union of two subclasses is a subclass. Theorem 27 of [Suppes] p. 27 and its converse. (Contributed by NM, 11-Jun-2004.)

Assertion

Ref	Expression
unss	⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)

Proof of Theorem unss

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ss 3917	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1871	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4132	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1820	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		df-ss 3917	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		df-ss 3917	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
7	5, 6	anbi12i 628	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
8	2, 4, 7	3bitr4i 303	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
9	1, 8	bitr2i 276	1 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1539   ∈ wcel 2110   ∪ cun 3898   ⊆ wss 3900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3436  df-un 3905  df-ss 3917

This theorem is referenced by:  unssi  4139  unssd  4140  unssad  4141  unssbd  4142  nsspssun  4216  uneqin  4237  prssg  4769  ssunsn2  4777  tpss  4787  iunopeqop  5459  eqrelrel  5735  xpsspw  5747  relun  5749  relcoi2  6220  pwuncl  7698  fnsuppres  8116  naddov3  8590  naddasslem1  8604  naddasslem2  8605  dfer2  8618  isinf  9144  trcl  9613  supxrun  13207  trclun  14913  isumltss  15747  rpnnen2lem12  16126  lcmfunsnlem  16544  lcmfun  16548  coprmprod  16564  coprmproddvdslem  16565  lubun  18413  isipodrs  18435  ipodrsima  18439  unocv  21610  aspval2  21828  uncld  22949  restntr  23090  cmpcld  23310  uncmp  23311  ufprim  23817  tsmsfbas  24036  ovolctb2  25413  ovolun  25420  unmbl  25458  plyun0  26122  noextendseq  27599  noresle  27629  madebdayim  27826  sshjcl  31325  sshjval2  31381  shlub  31384  ssjo  31417  spanuni  31514  tpssg  32507  cntzun  33038  unitprodclb  33344  tz9.1regs  35102  dfon2lem3  35798  dfon2lem7  35802  clsun  36341  lindsadd  37632  lindsenlbs  37634  mblfinlem3  37678  ismblfin  37680  paddssat  39832  pclunN  39916  paddunN  39945  poldmj1N  39946  pclfinclN  39968  lsmfgcl  43086  tfsconcatrnss  43362  ssuncl  43582  sssymdifcl  43584  undmrnresiss  43616  mptrcllem  43625  cnvrcl0  43637  dfrtrcl5  43641  brtrclfv2  43739  unhe1  43797  dffrege76  43951  uneqsn  44037  mnurndlem1  44293  gpgprismgr4cycllem8  48112  setrec1lem4  49701  elpglem2  49723