Theorem unss 4144

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 3923	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1900	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4138	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1849	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		df-ss 3923	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		df-ss 3923	. . . 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 1568   ∈ wcel 2143   ∪ cun 3904   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923

This theorem is referenced by:  unssi  4145  unssd  4146  unssad  4147  unssbd  4148  nsspssun  4222  uneqin  4243  prssg  4786  ssunsn2  4794  tpss  4803  iunopeqop  5506  iunopeqopOLD  5507  eqrelrel  5785  xpsspw  5798  relun  5800  relcoi2  6280  pwuncl  7770  fnsuppres  8188  naddov3  8668  naddasslem1  8682  naddasslem2  8683  dfer2  8696  isinf  9226  trcl  9698  supxrun  13343  trclun  15053  isumltss  15904  rpnnen2lem12  16282  lcmfunsnlem  16700  lcmfun  16704  coprmprod  16720  coprmproddvdslem  16721  lubun  18572  isipodrs  18594  ipodrsima  18598  unocv  21811  aspval2  22029  uncld  23179  restntr  23320  cmpcld  23540  uncmp  23541  ufprim  24047  tsmsfbas  24266  ovolctb2  25632  ovolun  25639  unmbl  25677  plyun0  26335  noextendseq  27812  noresle  27842  madebdayim  28062  sshjcl  31688  sshjval2  31744  shlub  31747  ssjo  31780  spanuni  31877  tpssg  32864  cntzun  33380  unitprodclb  33683  esplyind  33946  tz9.1regs  35528  dfon2lem3  36256  dfon2lem7  36260  clsun  36820  lindsadd  38245  lindsenlbs  38247  mblfinlem3  38291  ismblfin  38293  paddssat  40569  pclunN  40653  paddunN  40682  poldmj1N  40683  pclfinclN  40705  lsmfgcl  43784  tfsconcatrnss  44060  ssuncl  44279  sssymdifcl  44281  undmrnresiss  44313  mptrcllem  44322  cnvrcl0  44334  dfrtrcl5  44338  brtrclfv2  44436  unhe1  44494  dffrege76  44648  uneqsn  44734  mnurndlem1  44974  gpgprismgr4cycllem8  48850  setrec1lem4  50451  elpglem2  50473