Theorem ssequn2 3619

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 3616	. 2 |- ( A C_ B <-> ( A u. B ) = B )
2		uncom 3590	. . 3 |- ( A u. B ) = ( B u. A )
3	2	eqeq1i 2467	. 2 |- ( ( A u. B ) = B <-> ( B u. A ) = B )
4	1, 3	bitri 257	1 |- ( A C_ B <-> ( B u. A ) = B )

Syntax hints:   <-> wb 189   = wceq 1455   u. cun 3414   C_ wss 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-un 3421  df-in 3423  df-ss 3430

This theorem is referenced by:  unabs  3685  tppreqb  4126  pwssun  4759  pwundif  4760  relresfld  5381  relcoi1OLD  5384  ordssun  5541  ordequn  5542  oneluni  5554  fsnunf  6126  sorpssun  6605  ordunpr  6680  fodomr  7749  enp1ilem  7831  pwfilem  7894  brwdom2  8114  sucprcreg  8140  dfacfin7  8855  hashbclem  12648  incexclem  13943  ramub1lem1  15033  ramub1lem2  15034  mreexmrid  15598  lspun0  18283  lbsextlem4  18433  cldlp  20215  ordtuni  20255  lfinun  20589  cldsubg  21174  trust  21293  nulmbl2  22539  limcmpt2  22888  cnplimc  22891  dvreslem  22913  dvaddbr  22941  dvmulbr  22942  lhop  23017  plypf1  23215  coeeulem  23227  coeeu  23228  coef2  23234  rlimcnp  23940  ex-un  25923  shs0i  27151  chj0i  27157  disjun0  28254  ffsrn  28363  difioo  28413  eulerpartlemt  29253  subfacp1lem1  29951  cvmscld  30045  mthmpps  30269  refssfne  31063  topjoin  31070  poimirlem3  31988  poimirlem28  32013  rntrclfvOAI  35578  istopclsd  35587  nacsfix  35599  diophrw  35646  clcnvlem  36275  cnvrcl0  36277  dmtrcl  36279  rntrcl  36280  iunrelexp0  36339  dmtrclfvRP  36367  rntrclfv  36369  cotrclrcl  36379  limciccioolb  37739  limcicciooub  37755  ioccncflimc  37801  icocncflimc  37805  stoweidlem44  37943  dirkercncflem3  38005  fourierdlem62  38070  ismeannd  38343