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 1872	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4178	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1820	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		dfss2 3968	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		dfss2 3968	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
7	5, 6	anbi12i 626	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
8	2, 4, 7	3bitr4i 303	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
9	1, 8	bitr2i 276	1 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1538   ∈ wcel 2105   ∪ cun 3946   ⊆ wss 3948

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  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  5797  xpsspw  5809  relun  5811  relcoi2  6276  pwuncl  7761  fnsuppres  8181  wfrlem15OLD  8329  naddov3  8685  naddasslem1  8699  naddasslem2  8700  dfer2  8710  isinf  9266  isinfOLD  9267  trcl  9729  supxrun  13302  trclun  14968  isumltss  15801  rpnnen2lem12  16175  lcmfunsnlem  16585  lcmfun  16589  coprmprod  16605  coprmproddvdslem  16606  lubun  18475  isipodrs  18497  ipodrsima  18501  unocv  21456  aspval2  21675  uncld  22778  restntr  22919  cmpcld  23139  uncmp  23140  ufprim  23646  tsmsfbas  23865  ovolctb2  25254  ovolun  25261  unmbl  25299  plyun0  25960  noextendseq  27421  noresle  27451  madebdayim  27634  sshjcl  30890  sshjval2  30946  shlub  30949  ssjo  30982  spanuni  31079  cntzun  32497  dfon2lem3  35076  dfon2lem7  35080  clsun  35529  lindsadd  36797  lindsenlbs  36799  mblfinlem3  36843  ismblfin  36845  paddssat  39001  pclunN  39085  paddunN  39114  poldmj1N  39115  pclfinclN  39137  lsmfgcl  42131  tfsconcatrnss  42415  ssuncl  42636  sssymdifcl  42638  undmrnresiss  42670  mptrcllem  42679  cnvrcl0  42691  dfrtrcl5  42695  brtrclfv2  42793  unhe1  42851  dffrege76  43005  uneqsn  43091  mnurndlem1  43355  setrec1lem4  47835  elpglem2  47857