Theorem unss 4131

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 3907	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1872	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4125	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1821	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		df-ss 3907	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		df-ss 3907	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
7	5, 6	anbi12i 629	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
8	2, 4, 7	3bitr4i 303	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
9	1, 8	bitr2i 276	1 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   ∈ wcel 2114   ∪ cun 3888   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907

This theorem is referenced by:  unssi  4132  unssd  4133  unssad  4134  unssbd  4135  nsspssun  4209  uneqin  4230  prssg  4763  ssunsn2  4771  tpss  4781  iunopeqop  5469  eqrelrel  5746  xpsspw  5758  relun  5760  relcoi2  6235  pwuncl  7717  fnsuppres  8134  naddov3  8609  naddasslem1  8623  naddasslem2  8624  dfer2  8637  isinf  9168  trcl  9640  supxrun  13259  trclun  14967  isumltss  15804  rpnnen2lem12  16183  lcmfunsnlem  16601  lcmfun  16605  coprmprod  16621  coprmproddvdslem  16622  lubun  18472  isipodrs  18494  ipodrsima  18498  unocv  21670  aspval2  21888  uncld  23016  restntr  23157  cmpcld  23377  uncmp  23378  ufprim  23884  tsmsfbas  24103  ovolctb2  25469  ovolun  25476  unmbl  25514  plyun0  26172  noextendseq  27645  noresle  27675  madebdayim  27894  sshjcl  31441  sshjval2  31497  shlub  31500  ssjo  31533  spanuni  31630  tpssg  32622  cntzun  33155  unitprodclb  33464  esplyind  33734  tz9.1regs  35294  dfon2lem3  35981  dfon2lem7  35985  clsun  36526  lindsadd  37948  lindsenlbs  37950  mblfinlem3  37994  ismblfin  37996  paddssat  40274  pclunN  40358  paddunN  40387  poldmj1N  40388  pclfinclN  40410  lsmfgcl  43520  tfsconcatrnss  43796  ssuncl  44015  sssymdifcl  44017  undmrnresiss  44049  mptrcllem  44058  cnvrcl0  44070  dfrtrcl5  44074  brtrclfv2  44172  unhe1  44230  dffrege76  44384  uneqsn  44470  mnurndlem1  44726  gpgprismgr4cycllem8  48590  setrec1lem4  50177  elpglem2  50199