Theorem ssequn2 3645

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 3642	. 2 |- ( A C_ B <-> ( A u. B ) = B )
2		uncom 3616	. . 3 |- ( A u. B ) = ( B u. A )
3	2	eqeq1i 2436	. 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 3440   C_ wss 3442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-un 3447  df-in 3449  df-ss 3456

This theorem is referenced by:  unabs  3709  tppreqb  4144  pwssun  4760  pwundif  4761  relresfld  5382  relcoi1OLD  5385  ordssun  5541  ordequn  5542  oneluni  5554  fsnunf  6117  sorpssun  6592  ordunpr  6667  fodomr  7729  enp1ilem  7811  pwfilem  7874  brwdom2  8088  sucprcreg  8114  dfacfin7  8827  hashbclem  12610  incexclem  13872  ramub1lem1  14947  ramub1lem2  14948  mreexmrid  15500  lspun0  18169  lbsextlem4  18319  cldlp  20097  ordtuni  20137  lfinun  20471  cldsubg  21056  trust  21175  nulmbl2  22367  limcmpt2  22716  cnplimc  22719  dvreslem  22741  dvaddbr  22769  dvmulbr  22770  lhop  22845  plypf1  23034  coeeulem  23046  coeeu  23047  coef2  23053  rlimcnp  23756  ex-un  25719  shs0i  26937  chj0i  26943  disjun0  28044  ffsrn  28157  difioo  28200  eulerpartlemt  29030  subfacp1lem1  29690  cvmscld  29784  mthmpps  30008  refssfne  30799  topjoin  30806  poimirlem3  31646  poimirlem28  31671  rntrclfvOAI  35241  istopclsd  35250  nacsfix  35262  diophrw  35309  iunrelexp0  35932  dmtrclfvRP  35960  rntrclfv  35962  cotrclrcl  35972  limciccioolb  37272  limcicciooub  37288  ioccncflimc  37334  icocncflimc  37338  stoweidlem44  37473  dirkercncflem3  37535  fourierdlem62  37599  ismeannd  37813