Theorem unss 4160

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		dfss2 3955	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1871	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4154	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1820	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		dfss2 3955	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		dfss2 3955	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
7	5, 6	anbi12i 628	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
8	2, 4, 7	3bitr4i 305	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
9	1, 8	bitr2i 278	1 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1535   ∈ wcel 2114   ∪ cun 3934   ⊆ wss 3936

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-in 3943  df-ss 3952

This theorem is referenced by:  unssi  4161  unssd  4162  unssad  4163  unssbd  4164  nsspssun  4234  uneqin  4255  prssg  4752  ssunsn2  4760  tpss  4768  iunopeqop  5411  pwundifOLD  5457  eqrelrel  5670  xpsspw  5682  relun  5684  relcoi2  6128  pwuncl  7492  fnsuppres  7857  wfrlem15  7969  dfer2  8290  isinf  8731  trcl  9170  supxrun  12710  trclun  14374  isumltss  15203  rpnnen2lem12  15578  lcmfunsnlem  15985  lcmfun  15989  coprmprod  16005  coprmproddvdslem  16006  lubun  17733  isipodrs  17771  ipodrsima  17775  aspval2  20127  unocv  20824  uncld  21649  restntr  21790  cmpcld  22010  uncmp  22011  ufprim  22517  tsmsfbas  22736  ovolctb2  24093  ovolun  24100  unmbl  24138  plyun0  24787  sshjcl  29132  sshjval2  29188  shlub  29191  ssjo  29224  spanuni  29321  cntzun  30695  dfon2lem3  33030  dfon2lem7  33034  noextendseq  33174  noresle  33200  clsun  33676  lindsadd  34900  lindsenlbs  34902  mblfinlem3  34946  ismblfin  34948  paddssat  36965  pclunN  37049  paddunN  37078  poldmj1N  37079  pclfinclN  37101  lsmfgcl  39694  ssuncl  39949  sssymdifcl  39951  undmrnresiss  39984  mptrcllem  39993  cnvrcl0  40005  dfrtrcl5  40009  brtrclfv2  40092  unhe1  40151  dffrege76  40305  uneqsn  40393  mnurndlem1  40637  setrec1lem4  44813  elpglem2  44834