Theorem unss 4140

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 1871	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4134	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1820	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		df-ss 3919	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		df-ss 3919	. . . 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 2111   ∪ cun 3900   ⊆ wss 3902

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-ss 3919

This theorem is referenced by:  unssi  4141  unssd  4142  unssad  4143  unssbd  4144  nsspssun  4218  uneqin  4239  prssg  4771  ssunsn2  4779  tpss  4789  iunopeqop  5461  eqrelrel  5737  xpsspw  5749  relun  5751  relcoi2  6224  pwuncl  7703  fnsuppres  8121  naddov3  8595  naddasslem1  8609  naddasslem2  8610  dfer2  8623  isinf  9149  trcl  9618  supxrun  13212  trclun  14918  isumltss  15752  rpnnen2lem12  16131  lcmfunsnlem  16549  lcmfun  16553  coprmprod  16569  coprmproddvdslem  16570  lubun  18418  isipodrs  18440  ipodrsima  18444  unocv  21615  aspval2  21833  uncld  22954  restntr  23095  cmpcld  23315  uncmp  23316  ufprim  23822  tsmsfbas  24041  ovolctb2  25418  ovolun  25425  unmbl  25463  plyun0  26127  noextendseq  27604  noresle  27634  madebdayim  27831  sshjcl  31330  sshjval2  31386  shlub  31389  ssjo  31422  spanuni  31519  tpssg  32512  cntzun  33043  unitprodclb  33349  tz9.1regs  35118  dfon2lem3  35818  dfon2lem7  35822  clsun  36361  lindsadd  37652  lindsenlbs  37654  mblfinlem3  37698  ismblfin  37700  paddssat  39852  pclunN  39936  paddunN  39965  poldmj1N  39966  pclfinclN  39988  lsmfgcl  43106  tfsconcatrnss  43382  ssuncl  43602  sssymdifcl  43604  undmrnresiss  43636  mptrcllem  43645  cnvrcl0  43657  dfrtrcl5  43661  brtrclfv2  43759  unhe1  43817  dffrege76  43971  uneqsn  44057  mnurndlem1  44313  gpgprismgr4cycllem8  48132  setrec1lem4  49721  elpglem2  49743