Theorem unss 4146

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 3925	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1903	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4140	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1852	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		df-ss 3925	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		df-ss 3925	. . . 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 2146   ∪ cun 3906   ⊆ wss 3908

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-ss 3925

This theorem is used by:  unssi  4147  unssd  4148  unssad  4149  unssbd  4150  nsspssun  4224  uneqin  4245  prssg  4790  ssunsn2  4798  tpss  4807  iunopeqop  5509  iunopeqopOLD  5510  eqrelrel  5788  xpsspw  5801  relun  5803  relcoi2  6285  pwuncl  7778  fnsuppres  8196  naddov3  8676  naddasslem1  8690  naddasslem2  8691  dfer2  8704  isinf  9235  trcl  9707  supxrun  13360  trclun  15077  isumltss  15928  rpnnen2lem12  16306  lcmfunsnlem  16724  lcmfun  16728  coprmprod  16744  coprmproddvdslem  16745  lubun  18596  isipodrs  18618  ipodrsima  18622  unocv  21867  aspval2  22085  uncld  23235  restntr  23376  cmpcld  23596  uncmp  23597  ufprim  24103  tsmsfbas  24322  ovolctb2  25688  ovolun  25695  unmbl  25733  plyun0  26391  noextendseq  27868  noresle  27898  madebdayim  28118  sshjcl  31744  sshjval2  31800  shlub  31803  ssjo  31836  spanuni  31933  tpssg  32920  cntzun  33430  unitprodclb  33733  esplyind  33996  tz9.1regs  35571  dfon2lem3  36296  dfon2lem7  36300  clsun  36880  lindsadd  38305  lindsenlbs  38307  mblfinlem3  38351  ismblfin  38353  paddssat  40629  pclunN  40713  paddunN  40742  poldmj1N  40743  pclfinclN  40765  lsmfgcl  43842  tfsconcatrnss  44118  ssuncl  44337  sssymdifcl  44339  undmrnresiss  44371  mptrcllem  44380  cnvrcl0  44392  dfrtrcl5  44396  brtrclfv2  44494  unhe1  44552  dffrege76  44706  uneqsn  44792  mnurndlem1  45032  gpgprismgr4cycllem8  48908  setrec1lem4  50509  elpglem2  50531