Theorem ssequn2 3575

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

Assertion

Ref	Expression
ssequn2	|- ( A C_ B <-> ( B u. A ) = B )

Proof of Theorem ssequn2

Step	Hyp	Ref	Expression
1		ssequn1 3572	. 2 |- ( A C_ B <-> ( A u. B ) = B )
2		uncom 3546	. . 3 |- ( A u. B ) = ( B u. A )
3	2	eqeq1i 2427	. 2 |- ( ( A u. B ) = B <-> ( B u. A ) = B )
4	1, 3	bitri 252	1 |- ( A C_ B <-> ( B u. A ) = B )

Syntax hints:   <-> wb 187   = wceq 1437   u. cun 3370   C_ wss 3372

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-v 3018  df-un 3377  df-in 3379  df-ss 3386

This theorem is referenced by:  unabs  3639  tppreqb  4077  pwssun  4695  pwundif  4696  relresfld  5317  relcoi1OLD  5320  ordssun  5477  ordequn  5478  oneluni  5490  fsnunf  6054  sorpssun  6529  ordunpr  6604  fodomr  7669  enp1ilem  7751  pwfilem  7814  brwdom2  8034  sucprcreg  8060  dfacfin7  8773  hashbclem  12556  incexclem  13830  ramub1lem1  14920  ramub1lem2  14921  mreexmrid  15485  lspun0  18170  lbsextlem4  18320  cldlp  20101  ordtuni  20141  lfinun  20475  cldsubg  21060  trust  21179  nulmbl2  22425  limcmpt2  22774  cnplimc  22777  dvreslem  22799  dvaddbr  22827  dvmulbr  22828  lhop  22903  plypf1  23101  coeeulem  23113  coeeu  23114  coef2  23120  rlimcnp  23826  ex-un  25809  shs0i  27037  chj0i  27043  disjun0  28144  ffsrn  28257  difioo  28307  eulerpartlemt  29149  subfacp1lem1  29847  cvmscld  29941  mthmpps  30165  refssfne  30956  topjoin  30963  poimirlem3  31844  poimirlem28  31869  rntrclfvOAI  35439  istopclsd  35448  nacsfix  35460  diophrw  35507  clcnvlem  36137  cnvrcl0  36139  dmtrcl  36141  rntrcl  36142  iunrelexp0  36201  dmtrclfvRP  36229  rntrclfv  36231  cotrclrcl  36241  limciccioolb  37578  limcicciooub  37594  ioccncflimc  37640  icocncflimc  37644  stoweidlem44  37782  dirkercncflem3  37844  fourierdlem62  37909  ismeannd  38150