Theorem unss 4156

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 3934	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1870	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4150	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1819	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		df-ss 3934	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		df-ss 3934	. . . 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 1538   ∈ wcel 2109   ∪ cun 3915   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934

This theorem is referenced by:  unssi  4157  unssd  4158  unssad  4159  unssbd  4160  nsspssun  4234  uneqin  4255  prssg  4786  ssunsn2  4794  tpss  4804  iunopeqop  5484  eqrelrel  5763  xpsspw  5775  relun  5777  relcoi2  6253  pwuncl  7749  fnsuppres  8173  naddov3  8647  naddasslem1  8661  naddasslem2  8662  dfer2  8675  isinf  9214  isinfOLD  9215  trcl  9688  supxrun  13283  trclun  14987  isumltss  15821  rpnnen2lem12  16200  lcmfunsnlem  16618  lcmfun  16622  coprmprod  16638  coprmproddvdslem  16639  lubun  18481  isipodrs  18503  ipodrsima  18507  unocv  21596  aspval2  21814  uncld  22935  restntr  23076  cmpcld  23296  uncmp  23297  ufprim  23803  tsmsfbas  24022  ovolctb2  25400  ovolun  25407  unmbl  25445  plyun0  26109  noextendseq  27586  noresle  27616  madebdayim  27806  sshjcl  31291  sshjval2  31347  shlub  31350  ssjo  31383  spanuni  31480  tpssg  32473  cntzun  33015  unitprodclb  33367  dfon2lem3  35780  dfon2lem7  35784  clsun  36323  lindsadd  37614  lindsenlbs  37616  mblfinlem3  37660  ismblfin  37662  paddssat  39815  pclunN  39899  paddunN  39928  poldmj1N  39929  pclfinclN  39951  lsmfgcl  43070  tfsconcatrnss  43346  ssuncl  43566  sssymdifcl  43568  undmrnresiss  43600  mptrcllem  43609  cnvrcl0  43621  dfrtrcl5  43625  brtrclfv2  43723  unhe1  43781  dffrege76  43935  uneqsn  44021  mnurndlem1  44277  gpgprismgr4cycllem8  48096  setrec1lem4  49683  elpglem2  49705