Theorem unss 4136

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 3916	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1903	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4130	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1852	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		df-ss 3916	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		df-ss 3916	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
7	5, 6	anbi12i 640	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
8	2, 4, 7	3bitr4i 306	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
9	1, 8	bitr2i 279	1 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   ∈ wcel 2145   ∪ cun 3897   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916

This theorem is used by:  unssi  4137  unssd  4138  unssad  4139  unssbd  4140  nsspssun  4214  uneqin  4235  prssg  4780  ssunsn2  4788  tpss  4797  iunopeqop  5494  iunopeqopOLD  5495  eqrelrel  5773  xpsspw  5787  relun  5789  relcoi2  6273  pwuncl  7773  fnsuppres  8192  naddov3  8674  naddasslem1  8688  naddasslem2  8689  dfer2  8702  isinf  9240  trcl  9713  hfun  9899  setrec1lem4  9952  supxrun  13427  trclun  15147  isumltss  15997  rpnnen2lem12  16373  lcmfunsnlem  16796  lcmfun  16800  coprmprod  16816  coprmproddvdslem  16817  lubun  18669  isipodrs  18691  ipodrsima  18695  unocv  21966  lindsenlbs  22137  aspval2  22186  uncld  23339  restntr  23480  cmpcld  23700  uncmp  23701  ufprim  24208  tsmsfbas  24427  ovolctb2  25793  ovolun  25800  unmbl  25838  plyun0  26495  noextendseq  28006  noresle  28036  madebdayim  28256  sshjcl  31939  sshjval2  31995  shlub  31998  ssjo  32031  spanuni  32128  tpssg  33115  cntzun  33622  unitprodclb  33926  esplyind  34189  tz9.1regs  35775  dfon2lem3  36517  dfon2lem7  36521  clsun  37086  lindsadd  38504  mblfinlem3  38545  ismblfin  38547  paddssat  40839  pclunN  40923  paddunN  40952  poldmj1N  40953  pclfinclN  40975  lsmfgcl  44034  tfsconcatrnss  44310  ssuncl  44529  sssymdifcl  44531  undmrnresiss  44563  mptrcllem  44572  cnvrcl0  44584  dfrtrcl5  44588  brtrclfv2  44686  unhe1  44744  dffrege76  44898  uneqsn  44984  mnurndlem1  45224  gpgprismgr4cycllem8  49144  elpglem2  50749