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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   ∈ wcel 2145   ∪ cun 3900   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919

This theorem is used by:  unssi  4140  unssd  4141  unssad  4142  unssbd  4143  nsspssun  4217  uneqin  4238  prssg  4783  ssunsn2  4791  tpss  4800  iunopeqop  5502  iunopeqopOLD  5503  eqrelrel  5781  xpsspw  5794  relun  5796  relcoi2  6279  pwuncl  7773  fnsuppres  8193  naddov3  8673  naddasslem1  8687  naddasslem2  8688  dfer2  8701  isinf  9239  trcl  9711  supxrun  13372  trclun  15091  isumltss  15941  rpnnen2lem12  16319  lcmfunsnlem  16737  lcmfun  16741  coprmprod  16757  coprmproddvdslem  16758  lubun  18609  isipodrs  18631  ipodrsima  18635  unocv  21899  lindsenlbs  22070  aspval2  22119  uncld  23272  restntr  23413  cmpcld  23633  uncmp  23634  ufprim  24141  tsmsfbas  24360  ovolctb2  25726  ovolun  25733  unmbl  25771  plyun0  26429  noextendseq  27911  noresle  27941  madebdayim  28161  sshjcl  31844  sshjval2  31900  shlub  31903  ssjo  31936  spanuni  32033  tpssg  33020  cntzun  33527  unitprodclb  33830  esplyind  34093  tz9.1regs  35668  dfon2lem3  36370  dfon2lem7  36374  clsun  36955  lindsadd  38375  mblfinlem3  38416  ismblfin  38418  paddssat  40695  pclunN  40779  paddunN  40808  poldmj1N  40809  pclfinclN  40831  lsmfgcl  43923  tfsconcatrnss  44199  ssuncl  44418  sssymdifcl  44420  undmrnresiss  44452  mptrcllem  44461  cnvrcl0  44473  dfrtrcl5  44477  brtrclfv2  44575  unhe1  44633  dffrege76  44787  uneqsn  44873  mnurndlem1  45113  gpgprismgr4cycllem8  49026  setrec1lem4  50624  elpglem2  50646