Theorem unss 4153

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 3931	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1870	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4147	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1819	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		df-ss 3931	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		df-ss 3931	. . . 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 3912   ⊆ wss 3914

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931

This theorem is referenced by:  unssi  4154  unssd  4155  unssad  4156  unssbd  4157  nsspssun  4231  uneqin  4252  prssg  4783  ssunsn2  4791  tpss  4801  iunopeqop  5481  eqrelrel  5760  xpsspw  5772  relun  5774  relcoi2  6250  pwuncl  7746  fnsuppres  8170  naddov3  8644  naddasslem1  8658  naddasslem2  8659  dfer2  8672  isinf  9207  isinfOLD  9208  trcl  9681  supxrun  13276  trclun  14980  isumltss  15814  rpnnen2lem12  16193  lcmfunsnlem  16611  lcmfun  16615  coprmprod  16631  coprmproddvdslem  16632  lubun  18474  isipodrs  18496  ipodrsima  18500  unocv  21589  aspval2  21807  uncld  22928  restntr  23069  cmpcld  23289  uncmp  23290  ufprim  23796  tsmsfbas  24015  ovolctb2  25393  ovolun  25400  unmbl  25438  plyun0  26102  noextendseq  27579  noresle  27609  madebdayim  27799  sshjcl  31284  sshjval2  31340  shlub  31343  ssjo  31376  spanuni  31473  tpssg  32466  cntzun  33008  unitprodclb  33360  dfon2lem3  35773  dfon2lem7  35777  clsun  36316  lindsadd  37607  lindsenlbs  37609  mblfinlem3  37653  ismblfin  37655  paddssat  39808  pclunN  39892  paddunN  39921  poldmj1N  39922  pclfinclN  39944  lsmfgcl  43063  tfsconcatrnss  43339  ssuncl  43559  sssymdifcl  43561  undmrnresiss  43593  mptrcllem  43602  cnvrcl0  43614  dfrtrcl5  43618  brtrclfv2  43716  unhe1  43774  dffrege76  43928  uneqsn  44014  mnurndlem1  44270  gpgprismgr4cycllem8  48092  setrec1lem4  49679  elpglem2  49701