Theorem unss 4184

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 3968	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1874	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4178	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1822	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		dfss2 3968	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		dfss2 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 205   ∧ wa 397  ∀wal 1540   ∈ wcel 2107   ∪ cun 3946   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3953  df-in 3955  df-ss 3965

This theorem is referenced by:  unssi  4185  unssd  4186  unssad  4187  unssbd  4188  nsspssun  4257  uneqin  4278  prssg  4822  ssunsn2  4830  tpss  4838  iunopeqop  5521  eqrelrel  5796  xpsspw  5808  relun  5810  relcoi2  6274  pwuncl  7754  fnsuppres  8173  wfrlem15OLD  8320  naddov3  8676  naddasslem1  8690  naddasslem2  8691  dfer2  8701  isinf  9257  isinfOLD  9258  trcl  9720  supxrun  13292  trclun  14958  isumltss  15791  rpnnen2lem12  16165  lcmfunsnlem  16575  lcmfun  16579  coprmprod  16595  coprmproddvdslem  16596  lubun  18465  isipodrs  18487  ipodrsima  18491  unocv  21225  aspval2  21444  uncld  22537  restntr  22678  cmpcld  22898  uncmp  22899  ufprim  23405  tsmsfbas  23624  ovolctb2  25001  ovolun  25008  unmbl  25046  plyun0  25703  noextendseq  27160  noresle  27190  madebdayim  27372  sshjcl  30596  sshjval2  30652  shlub  30655  ssjo  30688  spanuni  30785  cntzun  32200  dfon2lem3  34746  dfon2lem7  34750  clsun  35202  lindsadd  36470  lindsenlbs  36472  mblfinlem3  36516  ismblfin  36518  paddssat  38674  pclunN  38758  paddunN  38787  poldmj1N  38788  pclfinclN  38810  lsmfgcl  41802  tfsconcatrnss  42086  ssuncl  42307  sssymdifcl  42309  undmrnresiss  42341  mptrcllem  42350  cnvrcl0  42362  dfrtrcl5  42366  brtrclfv2  42464  unhe1  42522  dffrege76  42676  uneqsn  42762  mnurndlem1  43026  setrec1lem4  47689  elpglem2  47711