Theorem unss 4139

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 3915	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1871	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4133	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1820	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		df-ss 3915	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		df-ss 3915	. . . 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 2113   ∪ cun 3896   ⊆ wss 3898

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-ss 3915

This theorem is referenced by:  unssi  4140  unssd  4141  unssad  4142  unssbd  4143  nsspssun  4217  uneqin  4238  prssg  4770  ssunsn2  4778  tpss  4788  iunopeqop  5464  eqrelrel  5741  xpsspw  5753  relun  5755  relcoi2  6229  pwuncl  7709  fnsuppres  8127  naddov3  8601  naddasslem1  8615  naddasslem2  8616  dfer2  8629  isinf  9156  trcl  9625  supxrun  13217  trclun  14923  isumltss  15757  rpnnen2lem12  16136  lcmfunsnlem  16554  lcmfun  16558  coprmprod  16574  coprmproddvdslem  16575  lubun  18423  isipodrs  18445  ipodrsima  18449  unocv  21619  aspval2  21837  uncld  22957  restntr  23098  cmpcld  23318  uncmp  23319  ufprim  23825  tsmsfbas  24044  ovolctb2  25421  ovolun  25428  unmbl  25466  plyun0  26130  noextendseq  27607  noresle  27637  madebdayim  27834  sshjcl  31337  sshjval2  31393  shlub  31396  ssjo  31429  spanuni  31526  tpssg  32519  cntzun  33055  unitprodclb  33361  esplyind  33613  tz9.1regs  35151  dfon2lem3  35848  dfon2lem7  35852  clsun  36393  lindsadd  37673  lindsenlbs  37675  mblfinlem3  37719  ismblfin  37721  paddssat  39933  pclunN  40017  paddunN  40046  poldmj1N  40047  pclfinclN  40069  lsmfgcl  43191  tfsconcatrnss  43467  ssuncl  43687  sssymdifcl  43689  undmrnresiss  43721  mptrcllem  43730  cnvrcl0  43742  dfrtrcl5  43746  brtrclfv2  43844  unhe1  43902  dffrege76  44056  uneqsn  44142  mnurndlem1  44398  gpgprismgr4cycllem8  48226  setrec1lem4  49815  elpglem2  49837