Theorem ssequn2 4118

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

Syntax hints:   ↔ wb 205   = wceq 1539   ∪ cun 3886   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-un 3893  df-in 3895  df-ss 3905

This theorem is referenced by:  unabs  4189  tppreqb  4739  pwssun  5486  pwundifOLD  5487  cnvimassrndm  6060  relresfld  6183  ordssun  6369  ordequn  6370  onun2  6374  oneluni  6383  fsnunf  7066  sorpssun  7592  ordunpr  7682  fodomr  8924  unfi  8964  pwfilem  8969  enp1ilem  9060  pwfilemOLD  9122  brwdom2  9341  sucprcreg  9369  dfacfin7  10164  hashbclem  14173  incexclem  15557  ramub1lem1  16736  ramub1lem2  16737  mreexmrid  17361  lspun0  20282  lbsextlem4  20432  cldlp  22310  ordtuni  22350  lfinun  22685  cldsubg  23271  trust  23390  nulmbl2  24709  limcmpt2  25057  cnplimc  25060  dvreslem  25082  dvaddbr  25111  dvmulbr  25112  lhop  25189  plypf1  25382  coeeulem  25394  coeeu  25395  coef2  25401  rlimcnp  26124  ex-un  28797  shs0i  29820  chj0i  29826  disjun0  30943  ffsrn  31073  difioo  31112  symgcom2  31362  eulerpartlemt  32347  fineqvac  33075  subfacp1lem1  33150  cvmscld  33244  mthmpps  33553  onunel  33698  noetalem1  33953  refssfne  34556  topjoin  34563  pibt2  35597  poimirlem3  35789  poimirlem28  35814  rntrclfvOAI  40520  istopclsd  40529  nacsfix  40541  diophrw  40588  clcnvlem  41238  cnvrcl0  41240  dmtrcl  41242  rntrcl  41243  iunrelexp0  41317  dmtrclfvRP  41345  rntrclfv  41347  cotrclrcl  41357  clsk3nimkb  41657  limciccioolb  43169  limcicciooub  43185  ioccncflimc  43433  icocncflimc  43437  stoweidlem44  43592  dirkercncflem3  43653  fourierdlem62  43716  ismeannd  44012