Theorem ssequn1 3673

Description: A relationship between subclass and union. Theorem 26 of [Suppes] p. 27. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
ssequn1

Proof of Theorem ssequn1

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bicom 200	. . . 4
2		pm4.72 876	. . . 4
3		elun 3644	. . . . 5
4	3	bibi1i 314	. . . 4
5	1, 2, 4	3bitr4i 277	. . 3
6	5	albii 1640	. 2
7		dfss2 3492	. 2
8		dfcleq 2450	. 2
9	6, 7, 8	3bitr4i 277	1

Syntax hints:  ->wi 4  <->wb 184  \/wo 368  A.wal 1393  =wceq 1395  e.wcel 1818  u.cun 3473  C_wss 3475

This theorem is referenced by:  ssequn2  3676  undif  3908  uniop  4755  pwssun  4791  unisuc  4959  ordssun  4982  ordequn  4983  onun2i  4998  funiunfv  6160  sorpssun  6587  ordunpr  6661  onuninsuci  6675  domss2  7696  sucdom2  7734  findcard2s  7781  rankopb  8291  ranksuc  8304  kmlem11  8561  fin1a2lem10  8810  modfsummods  13607  cvgcmpce  13632  mreexexlem3d  15043  dprd2da  17091  dpjcntz  17101  dpjdisj  17102  dpjlsm  17103  dpjidcl  17107  dpjidclOLD  17114  ablfac1eu  17124  perfcls  19866  dfcon2  19920  comppfsc  20033  llycmpkgen2  20051  trfil2  20388  fixufil  20423  tsmsresOLD  20645  tsmsres  20646  ustssco  20717  ustuqtop1  20744  xrge0gsumle  21338  volsup  21966  mbfss  22053  itg2cnlem2  22169  iblss2  22212  vieta1lem2  22707  amgm  23320  wilthlem2  23343  ftalem3  23348  rpvmasum2  23697  iuninc  27428  rankaltopb  29629  hfun  29835  nacsfix  30644  aacllem  33216  trclubg  37785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-in 3482  df-ss 3489