Theorem ssequn2 4159

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 4156	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		uncom 4129	. . 3 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	2	eqeq1i 2826	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
4	1, 3	bitri 277	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)

Syntax hints:   ↔ wb 208   = wceq 1537   ∪ cun 3934   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-in 3943  df-ss 3952

This theorem is referenced by:  unabs  4231  tppreqb  4738  pwssun  5456  pwundifOLD  5457  relresfld  6127  ordssun  6290  ordequn  6291  oneluni  6303  fsnunf  6947  sorpssun  7456  ordunpr  7541  fodomr  8668  enp1ilem  8752  pwfilem  8818  brwdom2  9037  sucprcreg  9065  dfacfin7  9821  hashbclem  13811  incexclem  15191  ramub1lem1  16362  ramub1lem2  16363  mreexmrid  16914  lspun0  19783  lbsextlem4  19933  cldlp  21758  ordtuni  21798  lfinun  22133  cldsubg  22719  trust  22838  nulmbl2  24137  limcmpt2  24482  cnplimc  24485  dvreslem  24507  dvaddbr  24535  dvmulbr  24536  lhop  24613  plypf1  24802  coeeulem  24814  coeeu  24815  coef2  24821  rlimcnp  25543  ex-un  28203  shs0i  29226  chj0i  29232  disjun0  30345  ffsrn  30465  difioo  30505  symgcom2  30728  eulerpartlemt  31629  subfacp1lem1  32426  cvmscld  32520  mthmpps  32829  refssfne  33706  topjoin  33713  pibt2  34701  poimirlem3  34910  poimirlem28  34935  rntrclfvOAI  39308  istopclsd  39317  nacsfix  39329  diophrw  39376  clcnvlem  40003  cnvrcl0  40005  dmtrcl  40007  rntrcl  40008  iunrelexp0  40067  dmtrclfvRP  40095  rntrclfv  40097  cotrclrcl  40107  clsk3nimkb  40410  limciccioolb  41922  limcicciooub  41938  ioccncflimc  42188  icocncflimc  42192  stoweidlem44  42349  dirkercncflem3  42410  fourierdlem62  42473  ismeannd  42769