Theorem ssequn2 4199

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

Syntax hints:   ↔ wb 206   = wceq 1537   ∪ cun 3961   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-ss 3980

This theorem is referenced by:  unabs  4271  undifr  4489  tppreqb  4810  pwssun  5580  cnvimassrndm  6174  relresfld  6298  ordssun  6488  ordequn  6489  onunel  6491  onun2  6494  oneluni  6505  fsnunf  7205  sorpssun  7749  ordunpr  7846  omun  7910  fodomr  9167  unfi  9210  enp1ilem  9310  pwfilem  9354  fodomfir  9366  brwdom2  9611  sucprcreg  9639  dfacfin7  10437  hashbclem  14488  incexclem  15869  ramub1lem1  17060  ramub1lem2  17061  mreexmrid  17688  lspun0  21027  lbsextlem4  21181  cldlp  23174  ordtuni  23214  lfinun  23549  cldsubg  24135  trust  24254  nulmbl2  25585  limcmpt2  25934  cnplimc  25937  dvreslem  25959  dvaddbr  25989  dvmulbr  25990  dvmulbrOLD  25991  lhop  26070  plypf1  26266  coeeulem  26278  coeeu  26279  coef2  26285  rlimcnp  27023  noetalem1  27801  addsproplem2  28018  ex-un  30453  shs0i  31478  chj0i  31484  disjun0  32615  ffsrn  32747  difioo  32791  symgcom2  33087  eulerpartlemt  34353  fineqvac  35090  subfacp1lem1  35164  cvmscld  35258  mthmpps  35567  refssfne  36341  topjoin  36348  pibt2  37400  poimirlem3  37610  poimirlem28  37635  rntrclfvOAI  42679  istopclsd  42688  nacsfix  42700  diophrw  42747  tfsconcatb0  43334  onsucunipr  43362  oaun3  43372  clcnvlem  43613  cnvrcl0  43615  dmtrcl  43617  rntrcl  43618  iunrelexp0  43692  dmtrclfvRP  43720  rntrclfv  43722  cotrclrcl  43732  clsk3nimkb  44030  limciccioolb  45577  limcicciooub  45593  ioccncflimc  45841  icocncflimc  45845  stoweidlem44  46000  dirkercncflem3  46061  fourierdlem62  46124  ismeannd  46423