Theorem unss 4142

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 3918	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1871	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4136	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1820	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		df-ss 3918	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		df-ss 3918	. . . 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 3899   ⊆ wss 3901

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918

This theorem is referenced by:  unssi  4143  unssd  4144  unssad  4145  unssbd  4146  nsspssun  4220  uneqin  4241  prssg  4775  ssunsn2  4783  tpss  4793  iunopeqop  5469  eqrelrel  5746  xpsspw  5758  relun  5760  relcoi2  6235  pwuncl  7715  fnsuppres  8133  naddov3  8608  naddasslem1  8622  naddasslem2  8623  dfer2  8636  isinf  9165  trcl  9637  supxrun  13231  trclun  14937  isumltss  15771  rpnnen2lem12  16150  lcmfunsnlem  16568  lcmfun  16572  coprmprod  16588  coprmproddvdslem  16589  lubun  18438  isipodrs  18460  ipodrsima  18464  unocv  21635  aspval2  21854  uncld  22985  restntr  23126  cmpcld  23346  uncmp  23347  ufprim  23853  tsmsfbas  24072  ovolctb2  25449  ovolun  25456  unmbl  25494  plyun0  26158  noextendseq  27635  noresle  27665  madebdayim  27884  sshjcl  31430  sshjval2  31486  shlub  31489  ssjo  31522  spanuni  31619  tpssg  32612  cntzun  33161  unitprodclb  33470  esplyind  33731  tz9.1regs  35290  dfon2lem3  35977  dfon2lem7  35981  clsun  36522  lindsadd  37810  lindsenlbs  37812  mblfinlem3  37856  ismblfin  37858  paddssat  40070  pclunN  40154  paddunN  40183  poldmj1N  40184  pclfinclN  40206  lsmfgcl  43312  tfsconcatrnss  43588  ssuncl  43807  sssymdifcl  43809  undmrnresiss  43841  mptrcllem  43850  cnvrcl0  43862  dfrtrcl5  43866  brtrclfv2  43964  unhe1  44022  dffrege76  44176  uneqsn  44262  mnurndlem1  44518  gpgprismgr4cycllem8  48344  setrec1lem4  49931  elpglem2  49953