Theorem unss 4151

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 3930	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1897	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4145	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1846	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		df-ss 3930	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		df-ss 3930	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
7	5, 6	anbi12i 639	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
8	2, 4, 7	3bitr4i 306	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
9	1, 8	bitr2i 279	1 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1565   ∈ wcel 2149   ∪ cun 3911   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930

This theorem is referenced by:  unssi  4152  unssd  4153  unssad  4154  unssbd  4155  nsspssun  4229  uneqin  4250  prssg  4786  ssunsn2  4794  tpss  4803  iunopeqop  5502  iunopeqopOLD  5503  eqrelrel  5781  xpsspw  5794  relun  5796  relcoi2  6276  pwuncl  7765  fnsuppres  8183  naddov3  8663  naddasslem1  8677  naddasslem2  8678  dfer2  8691  isinf  9221  trcl  9693  supxrun  13338  trclun  15047  isumltss  15898  rpnnen2lem12  16277  lcmfunsnlem  16695  lcmfun  16699  coprmprod  16715  coprmproddvdslem  16716  lubun  18567  isipodrs  18589  ipodrsima  18593  unocv  21795  aspval2  22013  uncld  23163  restntr  23304  cmpcld  23524  uncmp  23525  ufprim  24031  tsmsfbas  24250  ovolctb2  25616  ovolun  25623  unmbl  25661  plyun0  26319  noextendseq  27793  noresle  27823  madebdayim  28043  sshjcl  31644  sshjval2  31700  shlub  31703  ssjo  31736  spanuni  31833  tpssg  32820  cntzun  33336  unitprodclb  33642  esplyind  33906  tz9.1regs  35466  dfon2lem3  36170  dfon2lem7  36174  clsun  36724  lindsadd  38147  lindsenlbs  38149  mblfinlem3  38193  ismblfin  38195  paddssat  40473  pclunN  40557  paddunN  40586  poldmj1N  40587  pclfinclN  40609  lsmfgcl  43688  tfsconcatrnss  43964  ssuncl  44183  sssymdifcl  44185  undmrnresiss  44217  mptrcllem  44226  cnvrcl0  44238  dfrtrcl5  44242  brtrclfv2  44340  unhe1  44398  dffrege76  44552  uneqsn  44638  mnurndlem1  44878  gpgprismgr4cycllem8  48751  setrec1lem4  50348  elpglem2  50370