Theorem unss 4165

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538   ∈ wcel 2108   ∪ cun 3924   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943

This theorem is referenced by:  unssi  4166  unssd  4167  unssad  4168  unssbd  4169  nsspssun  4243  uneqin  4264  prssg  4795  ssunsn2  4803  tpss  4813  iunopeqop  5496  eqrelrel  5776  xpsspw  5788  relun  5790  relcoi2  6266  pwuncl  7764  fnsuppres  8190  wfrlem15OLD  8337  naddov3  8692  naddasslem1  8706  naddasslem2  8707  dfer2  8720  isinf  9268  isinfOLD  9269  trcl  9742  supxrun  13332  trclun  15033  isumltss  15864  rpnnen2lem12  16243  lcmfunsnlem  16660  lcmfun  16664  coprmprod  16680  coprmproddvdslem  16681  lubun  18525  isipodrs  18547  ipodrsima  18551  unocv  21640  aspval2  21858  uncld  22979  restntr  23120  cmpcld  23340  uncmp  23341  ufprim  23847  tsmsfbas  24066  ovolctb2  25445  ovolun  25452  unmbl  25490  plyun0  26154  noextendseq  27631  noresle  27661  madebdayim  27851  sshjcl  31336  sshjval2  31392  shlub  31395  ssjo  31428  spanuni  31525  tpssg  32518  cntzun  33062  unitprodclb  33404  dfon2lem3  35803  dfon2lem7  35807  clsun  36346  lindsadd  37637  lindsenlbs  37639  mblfinlem3  37683  ismblfin  37685  paddssat  39833  pclunN  39917  paddunN  39946  poldmj1N  39947  pclfinclN  39969  lsmfgcl  43098  tfsconcatrnss  43374  ssuncl  43594  sssymdifcl  43596  undmrnresiss  43628  mptrcllem  43637  cnvrcl0  43649  dfrtrcl5  43653  brtrclfv2  43751  unhe1  43809  dffrege76  43963  uneqsn  44049  mnurndlem1  44305  gpgprismgr4cycllem8  48101  setrec1lem4  49554  elpglem2  49576