Theorem ssequn2 4142

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 4139	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		uncom 4111	. . 3 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	2	eqeq1i 2742	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
4	1, 3	bitri 275	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)

Syntax hints:   ↔ wb 206   = wceq 1542   ∪ cun 3900   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-un 3907  df-ss 3919

This theorem is referenced by:  unabs  4218  undifr  4436  tppreqb  4762  pwssun  5517  cnvimassrndm  6111  relresfld  6235  ordssun  6422  ordequn  6423  onunel  6425  onun2  6428  oneluni  6438  fsnunf  7133  sorpssun  7677  ordunpr  7770  omun  7832  fodomr  9060  unfi  9099  enp1ilem  9182  pwfilem  9222  fodomfir  9232  brwdom2  9482  sucprcreg  9513  dfacfin7  10313  hashbclem  14379  incexclem  15763  ramub1lem1  16958  ramub1lem2  16959  mreexmrid  17570  lspun0  20966  lbsextlem4  21120  cldlp  23098  ordtuni  23138  lfinun  23473  cldsubg  24059  trust  24177  nulmbl2  25497  limcmpt2  25845  cnplimc  25848  dvreslem  25870  dvaddbr  25900  dvmulbr  25901  dvmulbrOLD  25902  lhop  25981  plypf1  26177  coeeulem  26189  coeeu  26190  coef2  26196  rlimcnp  26935  noetalem1  27713  addsproplem2  27952  ex-un  30482  shs0i  31507  chj0i  31513  disjun0  32652  ffsrn  32788  difioo  32843  symgcom2  33147  eulerpartlemt  34509  fineqvac  35253  subfacp1lem1  35354  cvmscld  35448  mthmpps  35757  refssfne  36533  topjoin  36540  pibt2  37593  poimirlem3  37795  poimirlem28  37820  rntrclfvOAI  42969  istopclsd  42978  nacsfix  42990  diophrw  43037  tfsconcatb0  43622  onsucunipr  43650  oaun3  43660  clcnvlem  43900  cnvrcl0  43902  dmtrcl  43904  rntrcl  43905  iunrelexp0  43979  dmtrclfvRP  44007  rntrclfv  44009  cotrclrcl  44019  clsk3nimkb  44317  limciccioolb  45903  limcicciooub  45917  ioccncflimc  46165  icocncflimc  46169  stoweidlem44  46324  dirkercncflem3  46385  fourierdlem62  46448  ismeannd  46747  cycl3grtri  48229