Theorem ssequn2 4144

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 4141	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		uncom 4114	. . 3 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	2	eqeq1i 2770	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
4	1, 3	bitri 278	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)

Syntax hints:   ↔ wb 209   = wceq 1563   ∪ cun 3905   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924

This theorem is referenced by:  unabs  4220  undifr  4440  tppreqb  4768  pwssun  5544  cnvimassrndm  6141  relresfld  6267  ordssun  6454  ordequn  6455  onunel  6457  onun2  6460  oneluni  6470  fsnunf  7173  sorpssun  7717  ordunpr  7810  omun  7872  fodomr  9104  unfi  9143  enp1ilem  9226  pwfilem  9265  fodomfir  9275  brwdom2  9523  sucprcreg  9556  sucprcregOLD  9557  dfacfin7  10371  hashbclem  14479  incexclem  15880  ramub1lem1  17076  ramub1lem2  17077  mreexmrid  17689  lspun0  21101  lbsextlem4  21254  cldlp  23268  ordtuni  23308  lfinun  23643  cldsubg  24229  trust  24347  nulmbl2  25656  limcmpt2  26004  cnplimc  26007  dvreslem  26029  dvaddbr  26058  dvmulbr  26059  lhop  26136  plypf1  26330  coeeulem  26342  coeeu  26343  coef2  26349  rlimcnp  27088  noetalem1  27863  addsproplem2  28121  ex-un  30684  shs0i  31710  chj0i  31716  disjun0  32850  ffsrn  32985  difioo  33039  symgcom2  33317  eulerpartlemt  34678  fineqvac  35424  subfacp1lem1  35542  cvmscld  35636  mthmpps  35945  refssfne  36731  topjoin  36738  pibt2  37923  poimirlem3  38134  poimirlem28  38159  rntrclfvOAI  43284  istopclsd  43293  nacsfix  43305  diophrw  43352  tfsconcatb0  43933  onsucunipr  43961  oaun3  43971  clcnvlem  44211  cnvrcl0  44213  dmtrcl  44215  rntrcl  44216  iunrelexp0  44290  dmtrclfvRP  44318  rntrclfv  44320  cotrclrcl  44330  clsk3nimkb  44628  limciccioolb  46195  limcicciooub  46209  ioccncflimc  46457  icocncflimc  46461  stoweidlem44  46616  dirkercncflem3  46677  fourierdlem62  46740  ismeannd  47039  cycl3grtri  48567