Theorem unss 4144

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 3920	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1872	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4138	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1821	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		df-ss 3920	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		df-ss 3920	. . . 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 3901   ⊆ wss 3903

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920

This theorem is referenced by:  unssi  4145  unssd  4146  unssad  4147  unssbd  4148  nsspssun  4222  uneqin  4243  prssg  4777  ssunsn2  4785  tpss  4795  iunopeqop  5477  eqrelrel  5754  xpsspw  5766  relun  5768  relcoi2  6243  pwuncl  7725  fnsuppres  8143  naddov3  8618  naddasslem1  8632  naddasslem2  8633  dfer2  8646  isinf  9177  trcl  9649  supxrun  13243  trclun  14949  isumltss  15783  rpnnen2lem12  16162  lcmfunsnlem  16580  lcmfun  16584  coprmprod  16600  coprmproddvdslem  16601  lubun  18450  isipodrs  18472  ipodrsima  18476  unocv  21647  aspval2  21866  uncld  22997  restntr  23138  cmpcld  23358  uncmp  23359  ufprim  23865  tsmsfbas  24084  ovolctb2  25461  ovolun  25468  unmbl  25506  plyun0  26170  noextendseq  27647  noresle  27677  madebdayim  27896  sshjcl  31442  sshjval2  31498  shlub  31501  ssjo  31534  spanuni  31631  tpssg  32623  cntzun  33172  unitprodclb  33481  esplyind  33751  tz9.1regs  35309  dfon2lem3  35996  dfon2lem7  36000  clsun  36541  lindsadd  37858  lindsenlbs  37860  mblfinlem3  37904  ismblfin  37906  paddssat  40184  pclunN  40268  paddunN  40297  poldmj1N  40298  pclfinclN  40320  lsmfgcl  43425  tfsconcatrnss  43701  ssuncl  43920  sssymdifcl  43922  undmrnresiss  43954  mptrcllem  43963  cnvrcl0  43975  dfrtrcl5  43979  brtrclfv2  44077  unhe1  44135  dffrege76  44289  uneqsn  44375  mnurndlem1  44631  gpgprismgr4cycllem8  48456  setrec1lem4  50043  elpglem2  50065