Theorem unss 4213

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1535   ∈ wcel 2108   ∪ cun 3974   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993

This theorem is referenced by:  unssi  4214  unssd  4215  unssad  4216  unssbd  4217  nsspssun  4287  uneqin  4308  prssg  4844  ssunsn2  4852  tpss  4862  iunopeqop  5540  eqrelrel  5821  xpsspw  5833  relun  5835  relcoi2  6308  pwuncl  7805  fnsuppres  8232  wfrlem15OLD  8379  naddov3  8736  naddasslem1  8750  naddasslem2  8751  dfer2  8764  isinf  9323  isinfOLD  9324  trcl  9797  supxrun  13378  trclun  15063  isumltss  15896  rpnnen2lem12  16273  lcmfunsnlem  16688  lcmfun  16692  coprmprod  16708  coprmproddvdslem  16709  lubun  18585  isipodrs  18607  ipodrsima  18611  unocv  21721  aspval2  21941  uncld  23070  restntr  23211  cmpcld  23431  uncmp  23432  ufprim  23938  tsmsfbas  24157  ovolctb2  25546  ovolun  25553  unmbl  25591  plyun0  26256  noextendseq  27730  noresle  27760  madebdayim  27944  sshjcl  31387  sshjval2  31443  shlub  31446  ssjo  31479  spanuni  31576  cntzun  33044  unitprodclb  33382  dfon2lem3  35749  dfon2lem7  35753  clsun  36294  lindsadd  37573  lindsenlbs  37575  mblfinlem3  37619  ismblfin  37621  paddssat  39771  pclunN  39855  paddunN  39884  poldmj1N  39885  pclfinclN  39907  lsmfgcl  43031  tfsconcatrnss  43312  ssuncl  43532  sssymdifcl  43534  undmrnresiss  43566  mptrcllem  43575  cnvrcl0  43587  dfrtrcl5  43591  brtrclfv2  43689  unhe1  43747  dffrege76  43901  uneqsn  43987  mnurndlem1  44250  setrec1lem4  48782  elpglem2  48804