Theorem unss 4199

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 3979	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1867	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4193	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1815	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		df-ss 3979	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		df-ss 3979	. . . 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 1534   ∈ wcel 2105   ∪ cun 3960   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-ss 3979

This theorem is referenced by:  unssi  4200  unssd  4201  unssad  4202  unssbd  4203  nsspssun  4273  uneqin  4294  prssg  4823  ssunsn2  4831  tpss  4841  iunopeqop  5530  eqrelrel  5809  xpsspw  5821  relun  5823  relcoi2  6298  pwuncl  7788  fnsuppres  8214  wfrlem15OLD  8361  naddov3  8716  naddasslem1  8730  naddasslem2  8731  dfer2  8744  isinf  9293  isinfOLD  9294  trcl  9765  supxrun  13354  trclun  15049  isumltss  15880  rpnnen2lem12  16257  lcmfunsnlem  16674  lcmfun  16678  coprmprod  16694  coprmproddvdslem  16695  lubun  18572  isipodrs  18594  ipodrsima  18598  unocv  21715  aspval2  21935  uncld  23064  restntr  23205  cmpcld  23425  uncmp  23426  ufprim  23932  tsmsfbas  24151  ovolctb2  25540  ovolun  25547  unmbl  25585  plyun0  26250  noextendseq  27726  noresle  27756  madebdayim  27940  sshjcl  31383  sshjval2  31439  shlub  31442  ssjo  31475  spanuni  31572  cntzun  33053  unitprodclb  33396  dfon2lem3  35766  dfon2lem7  35770  clsun  36310  lindsadd  37599  lindsenlbs  37601  mblfinlem3  37645  ismblfin  37647  paddssat  39796  pclunN  39880  paddunN  39909  poldmj1N  39910  pclfinclN  39932  lsmfgcl  43062  tfsconcatrnss  43339  ssuncl  43559  sssymdifcl  43561  undmrnresiss  43593  mptrcllem  43602  cnvrcl0  43614  dfrtrcl5  43618  brtrclfv2  43716  unhe1  43774  dffrege76  43928  uneqsn  44014  mnurndlem1  44276  setrec1lem4  48920  elpglem2  48942