Theorem ssequn2 4183

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 4180	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		uncom 4153	. . 3 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	2	eqeq1i 2737	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
4	1, 3	bitri 274	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)

Syntax hints:   ↔ wb 205   = wceq 1541   ∪ cun 3946   ⊆ wss 3948

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-in 3955  df-ss 3965

This theorem is referenced by:  unabs  4254  undifr  4482  tppreqb  4808  pwssun  5571  cnvimassrndm  6151  relresfld  6275  ordssun  6466  ordequn  6467  onunel  6469  onun2  6472  oneluni  6483  fsnunf  7185  sorpssun  7722  ordunpr  7816  omun  7880  fodomr  9130  unfi  9174  pwfilem  9179  enp1ilem  9280  pwfilemOLD  9348  brwdom2  9570  sucprcreg  9598  dfacfin7  10396  hashbclem  14413  incexclem  15784  ramub1lem1  16961  ramub1lem2  16962  mreexmrid  17589  lspun0  20627  lbsextlem4  20780  cldlp  22661  ordtuni  22701  lfinun  23036  cldsubg  23622  trust  23741  nulmbl2  25060  limcmpt2  25408  cnplimc  25411  dvreslem  25433  dvaddbr  25462  dvmulbr  25463  lhop  25540  plypf1  25733  coeeulem  25745  coeeu  25746  coef2  25752  rlimcnp  26477  noetalem1  27251  addsproplem2  27463  ex-un  29715  shs0i  30740  chj0i  30746  disjun0  31864  ffsrn  31992  difioo  32031  symgcom2  32286  eulerpartlemt  33439  fineqvac  34166  subfacp1lem1  34239  cvmscld  34333  mthmpps  34642  gg-dvmulbr  35244  refssfne  35329  topjoin  35336  pibt2  36384  poimirlem3  36577  poimirlem28  36602  rntrclfvOAI  41511  istopclsd  41520  nacsfix  41532  diophrw  41579  tfsconcatb0  42176  onsucunipr  42204  oaun3  42214  clcnvlem  42456  cnvrcl0  42458  dmtrcl  42460  rntrcl  42461  iunrelexp0  42535  dmtrclfvRP  42563  rntrclfv  42565  cotrclrcl  42575  clsk3nimkb  42873  limciccioolb  44416  limcicciooub  44432  ioccncflimc  44680  icocncflimc  44684  stoweidlem44  44839  dirkercncflem3  44900  fourierdlem62  44963  ismeannd  45262