Theorem unss 4145

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 3924	. 2 ⊢ ((𝐴 ∪ 𝐵) ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶))
2		19.26 1893	. . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
3		elunant 4139	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
4	3	albii 1842	. . 3 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
5		df-ss 3924	. . . 4 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))
6		df-ss 3924	. . . 4 ⊢ (𝐵 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶))
7	5, 6	anbi12i 639	. . 3 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶) ∧ ∀𝑥(𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐶)))
8	2, 4, 7	3bitr4i 306	. 2 ⊢ (∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) → 𝑥 ∈ 𝐶) ↔ (𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶))
9	1, 8	bitr2i 279	1 ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∪ 𝐵) ⊆ 𝐶)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1561   ∈ wcel 2145   ∪ cun 3905   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924

This theorem is referenced by:  unssi  4146  unssd  4147  unssad  4148  unssbd  4149  nsspssun  4223  uneqin  4244  prssg  4780  ssunsn2  4788  tpss  4798  iunopeqop  5495  iunopeqopOLD  5496  eqrelrel  5774  xpsspw  5787  relun  5789  relcoi2  6268  pwuncl  7757  fnsuppres  8175  naddov3  8655  naddasslem1  8669  naddasslem2  8670  dfer2  8683  isinf  9213  trcl  9685  supxrun  13333  trclun  15041  isumltss  15892  rpnnen2lem12  16271  lcmfunsnlem  16689  lcmfun  16693  coprmprod  16709  coprmproddvdslem  16710  lubun  18561  isipodrs  18583  ipodrsima  18587  unocv  21790  aspval2  22008  uncld  23159  restntr  23300  cmpcld  23520  uncmp  23521  ufprim  24027  tsmsfbas  24246  ovolctb2  25612  ovolun  25619  unmbl  25657  plyun0  26315  noextendseq  27789  noresle  27819  madebdayim  28039  sshjcl  31616  sshjval2  31672  shlub  31675  ssjo  31708  spanuni  31805  tpssg  32793  cntzun  33312  unitprodclb  33618  esplyind  33882  tz9.1regs  35442  dfon2lem3  36146  dfon2lem7  36150  clsun  36701  lindsadd  38124  lindsenlbs  38126  mblfinlem3  38170  ismblfin  38172  paddssat  40450  pclunN  40534  paddunN  40563  poldmj1N  40564  pclfinclN  40586  lsmfgcl  43663  tfsconcatrnss  43939  ssuncl  44158  sssymdifcl  44160  undmrnresiss  44192  mptrcllem  44201  cnvrcl0  44213  dfrtrcl5  44217  brtrclfv2  44315  unhe1  44373  dffrege76  44527  uneqsn  44613  mnurndlem1  44855  gpgprismgr4cycllem8  48722  setrec1lem4  50319  elpglem2  50341