Theorem unss 4114

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 3903	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1874	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4108	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1823	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		dfss2 3903	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		dfss2 3903	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
7	5, 6	anbi12i 626	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
8	2, 4, 7	3bitr4i 302	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
9	1, 8	bitr2i 275	1 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1537   ∈ wcel 2108   ∪ cun 3881   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900

This theorem is referenced by:  unssi  4115  unssd  4116  unssad  4117  unssbd  4118  nsspssun  4188  uneqin  4209  prssg  4749  ssunsn2  4757  tpss  4765  iunopeqop  5429  pwundifOLD  5477  eqrelrel  5696  xpsspw  5708  relun  5710  relcoi2  6169  pwuncl  7598  fnsuppres  7978  wfrlem15OLD  8125  dfer2  8457  isinf  8965  trcl  9417  supxrun  12979  trclun  14653  isumltss  15488  rpnnen2lem12  15862  lcmfunsnlem  16274  lcmfun  16278  coprmprod  16294  coprmproddvdslem  16295  lubun  18148  isipodrs  18170  ipodrsima  18174  unocv  20797  aspval2  21012  uncld  22100  restntr  22241  cmpcld  22461  uncmp  22462  ufprim  22968  tsmsfbas  23187  ovolctb2  24561  ovolun  24568  unmbl  24606  plyun0  25263  sshjcl  29618  sshjval2  29674  shlub  29677  ssjo  29710  spanuni  29807  cntzun  31222  dfon2lem3  33667  dfon2lem7  33671  noextendseq  33797  noresle  33827  madebdayim  33997  clsun  34444  lindsadd  35697  lindsenlbs  35699  mblfinlem3  35743  ismblfin  35745  paddssat  37755  pclunN  37839  paddunN  37868  poldmj1N  37869  pclfinclN  37891  lsmfgcl  40815  ssuncl  41066  sssymdifcl  41068  undmrnresiss  41101  mptrcllem  41110  cnvrcl0  41122  dfrtrcl5  41126  brtrclfv2  41224  unhe1  41282  dffrege76  41436  uneqsn  41522  mnurndlem1  41788  setrec1lem4  46282  elpglem2  46303