Theorem unss 4130

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 3906	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1872	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4124	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1821	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		df-ss 3906	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		df-ss 3906	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
7	5, 6	anbi12i 629	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
8	2, 4, 7	3bitr4i 303	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
9	1, 8	bitr2i 276	1 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   ∈ wcel 2114   ∪ cun 3887   ⊆ wss 3889

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906

This theorem is referenced by:  unssi  4131  unssd  4132  unssad  4133  unssbd  4134  nsspssun  4208  uneqin  4229  prssg  4762  ssunsn2  4770  tpss  4780  iunopeqop  5475  iunopeqopOLD  5476  eqrelrel  5753  xpsspw  5765  relun  5767  relcoi2  6241  pwuncl  7724  fnsuppres  8141  naddov3  8616  naddasslem1  8630  naddasslem2  8631  dfer2  8644  isinf  9175  trcl  9649  supxrun  13268  trclun  14976  isumltss  15813  rpnnen2lem12  16192  lcmfunsnlem  16610  lcmfun  16614  coprmprod  16630  coprmproddvdslem  16631  lubun  18481  isipodrs  18503  ipodrsima  18507  unocv  21660  aspval2  21878  uncld  23006  restntr  23147  cmpcld  23367  uncmp  23368  ufprim  23874  tsmsfbas  24093  ovolctb2  25459  ovolun  25466  unmbl  25504  plyun0  26162  noextendseq  27631  noresle  27661  madebdayim  27880  sshjcl  31426  sshjval2  31482  shlub  31485  ssjo  31518  spanuni  31615  tpssg  32607  cntzun  33140  unitprodclb  33449  esplyind  33719  tz9.1regs  35278  dfon2lem3  35965  dfon2lem7  35969  clsun  36510  lindsadd  37934  lindsenlbs  37936  mblfinlem3  37980  ismblfin  37982  paddssat  40260  pclunN  40344  paddunN  40373  poldmj1N  40374  pclfinclN  40396  lsmfgcl  43502  tfsconcatrnss  43778  ssuncl  43997  sssymdifcl  43999  undmrnresiss  44031  mptrcllem  44040  cnvrcl0  44052  dfrtrcl5  44056  brtrclfv2  44154  unhe1  44212  dffrege76  44366  uneqsn  44452  mnurndlem1  44708  gpgprismgr4cycllem8  48578  setrec1lem4  50165  elpglem2  50187