Theorem unss 4191

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   ∈ wcel 2147   ⊆ wss 3900   ∪ cun 4152

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154

This theorem is used by:  unssi  4192  unssd  4193  unssad  4194  unssbd  4195  nsspssun  4216  uneqin  4237  prssg  4778  ssunsn2  4786  tpss  4795  iunopeqop  5498  iunopeqopOLD  5499  eqrelrel  5778  xpsspw  5792  relun  5794  relcoi2  6298  pwuncl  7808  fnsuppres  8236  naddov3  8718  naddasslem1  8732  naddasslem2  8733  dfer2  8746  isinf  9284  trcl  9756  hfun  9945  setrec1lem4  9998  supxrun  13473  trclun  15196  isumltss  16046  rpnnen2lem12  16422  lcmfunsnlem  16845  lcmfun  16849  coprmprod  16865  coprmproddvdslem  16866  lubun  18718  isipodrs  18740  ipodrsima  18744  unocv  22016  lindsenlbs  22187  aspval2  22236  uncld  23389  restntr  23530  cmpcld  23750  uncmp  23751  ufprim  24258  tsmsfbas  24477  ovolctb2  25843  ovolun  25850  unmbl  25888  plyun0  26545  noextendseq  28054  noresle  28084  madebdayim  28304  sshjcl  31987  sshjval2  32043  shlub  32046  ssjo  32079  spanuni  32176  tpssg  33205  cntzun  33710  unitprodclb  34014  esplyind  34277  tz9.1regs  35902  dfon2lem3  36725  dfon2lem7  36729  clsun  37294  lindsadd  38728  mblfinlem3  38769  ismblfin  38771  paddssat  41063  pclunN  41147  paddunN  41176  poldmj1N  41177  pclfinclN  41199  lsmfgcl  44269  tfsconcatrnss  44544  ssuncl  44763  sssymdifcl  44765  undmrnresiss  44796  mptrcllem  44805  cnvrcl0  44817  dfrtrcl5  44821  brtrclfv2  44919  unhe1  44977  dffrege76  45131  uneqsn  45217  mnurndlem1  45457  gpgprismgr4cycllem8  49405  elpglem2  51085