Theorem unss 4190

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 3968	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1870	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4184	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1819	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		df-ss 3968	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		df-ss 3968	. . . 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 2108   ∪ cun 3949   ⊆ wss 3951

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968

This theorem is referenced by:  unssi  4191  unssd  4192  unssad  4193  unssbd  4194  nsspssun  4268  uneqin  4289  prssg  4819  ssunsn2  4827  tpss  4837  iunopeqop  5526  eqrelrel  5807  xpsspw  5819  relun  5821  relcoi2  6297  pwuncl  7790  fnsuppres  8216  wfrlem15OLD  8363  naddov3  8718  naddasslem1  8732  naddasslem2  8733  dfer2  8746  isinf  9296  isinfOLD  9297  trcl  9768  supxrun  13358  trclun  15053  isumltss  15884  rpnnen2lem12  16261  lcmfunsnlem  16678  lcmfun  16682  coprmprod  16698  coprmproddvdslem  16699  lubun  18560  isipodrs  18582  ipodrsima  18586  unocv  21698  aspval2  21918  uncld  23049  restntr  23190  cmpcld  23410  uncmp  23411  ufprim  23917  tsmsfbas  24136  ovolctb2  25527  ovolun  25534  unmbl  25572  plyun0  26236  noextendseq  27712  noresle  27742  madebdayim  27926  sshjcl  31374  sshjval2  31430  shlub  31433  ssjo  31466  spanuni  31563  cntzun  33071  unitprodclb  33417  dfon2lem3  35786  dfon2lem7  35790  clsun  36329  lindsadd  37620  lindsenlbs  37622  mblfinlem3  37666  ismblfin  37668  paddssat  39816  pclunN  39900  paddunN  39929  poldmj1N  39930  pclfinclN  39952  lsmfgcl  43086  tfsconcatrnss  43363  ssuncl  43583  sssymdifcl  43585  undmrnresiss  43617  mptrcllem  43626  cnvrcl0  43638  dfrtrcl5  43642  brtrclfv2  43740  unhe1  43798  dffrege76  43952  uneqsn  44038  mnurndlem1  44300  setrec1lem4  49209  elpglem2  49231