Theorem unss 4111

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 3901	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1871	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4105	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1821	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		dfss2 3901	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		dfss2 3901	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
7	5, 6	anbi12i 629	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
8	2, 4, 7	3bitr4i 306	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
9	1, 8	bitr2i 279	1 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   ∈ wcel 2111   ∪ cun 3879   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898

This theorem is referenced by:  unssi  4112  unssd  4113  unssad  4114  unssbd  4115  nsspssun  4184  uneqin  4205  prssg  4712  ssunsn2  4720  tpss  4728  iunopeqop  5376  pwundifOLD  5422  eqrelrel  5634  xpsspw  5646  relun  5648  relcoi2  6096  pwuncl  7472  fnsuppres  7840  wfrlem15  7952  dfer2  8273  isinf  8715  trcl  9154  supxrun  12697  trclun  14365  isumltss  15195  rpnnen2lem12  15570  lcmfunsnlem  15975  lcmfun  15979  coprmprod  15995  coprmproddvdslem  15996  lubun  17725  isipodrs  17763  ipodrsima  17767  unocv  20369  aspval2  20584  uncld  21646  restntr  21787  cmpcld  22007  uncmp  22008  ufprim  22514  tsmsfbas  22733  ovolctb2  24096  ovolun  24103  unmbl  24141  plyun0  24794  sshjcl  29138  sshjval2  29194  shlub  29197  ssjo  29230  spanuni  29327  cntzun  30745  dfon2lem3  33143  dfon2lem7  33147  noextendseq  33287  noresle  33313  clsun  33789  lindsadd  35050  lindsenlbs  35052  mblfinlem3  35096  ismblfin  35098  paddssat  37110  pclunN  37194  paddunN  37223  poldmj1N  37224  pclfinclN  37246  lsmfgcl  40018  ssuncl  40269  sssymdifcl  40271  undmrnresiss  40304  mptrcllem  40313  cnvrcl0  40325  dfrtrcl5  40329  brtrclfv2  40428  unhe1  40486  dffrege76  40640  uneqsn  40726  mnurndlem1  40989  setrec1lem4  45220  elpglem2  45241