Theorem ssequn2 3676

Description: A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.)

Assertion

Ref	Expression
ssequn2

Proof of Theorem ssequn2

Step	Hyp	Ref	Expression
1		ssequn1 3673	. 2
2		uncom 3647	. . 3
3	2	eqeq1i 2464	. 2
4	1, 3	bitri 249	1

Syntax hints:  <->wb 184  =wceq 1395  u.cun 3473  C_wss 3475

This theorem is referenced by:  unabs  3727  tppreqb  4171  pwssun  4791  pwundif  4792  ordssun  4982  ordequn  4983  oneluni  4995  relresfld  5539  relcoi1  5541  fsnunf  6109  sorpssun  6587  ordunpr  6661  fodomr  7688  enp1ilem  7774  pwfilem  7834  brwdom2  8020  sucprcreg  8046  dfacfin7  8800  hashbclem  12501  incexclem  13648  ramub1lem1  14544  ramub1lem2  14545  mreexmrid  15040  lspun0  17657  lbsextlem4  17807  cldlp  19651  ordtuni  19691  lfinun  20026  cldsubg  20609  trust  20732  nulmbl2  21947  limcmpt2  22288  cnplimc  22291  dvreslem  22313  dvaddbr  22341  dvmulbr  22342  lhop  22417  plypf1  22609  coeeulem  22621  coeeu  22622  coef2  22628  rlimcnp  23295  ex-un  25145  shs0i  26367  chj0i  26373  ffsrn  27552  difioo  27593  eulerpartlemt  28310  subfacp1lem1  28623  cvmscld  28718  mthmpps  28942  refssfne  30176  topjoin  30183  istopclsd  30632  nacsfix  30644  diophrw  30692  limciccioolb  31627  limcicciooub  31643  ioccncflimc  31688  icocncflimc  31692  stoweidlem44  31826  dirkercncflem3  31887  fourierdlem62  31951

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