Theorem ssequn2 4152

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∪ cun 3912   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931

This theorem is referenced by:  unabs  4228  undifr  4446  tppreqb  4769  pwssun  5530  cnvimassrndm  6125  relresfld  6249  ordssun  6436  ordequn  6437  onunel  6439  onun2  6442  oneluni  6453  fsnunf  7159  sorpssun  7706  ordunpr  7801  omun  7864  fodomr  9092  unfi  9135  enp1ilem  9223  pwfilem  9267  fodomfir  9279  brwdom2  9526  sucprcreg  9554  dfacfin7  10352  hashbclem  14417  incexclem  15802  ramub1lem1  16997  ramub1lem2  16998  mreexmrid  17604  lspun0  20917  lbsextlem4  21071  cldlp  23037  ordtuni  23077  lfinun  23412  cldsubg  23998  trust  24117  nulmbl2  25437  limcmpt2  25785  cnplimc  25788  dvreslem  25810  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  lhop  25921  plypf1  26117  coeeulem  26129  coeeu  26130  coef2  26136  rlimcnp  26875  noetalem1  27653  addsproplem2  27877  ex-un  30353  shs0i  31378  chj0i  31384  disjun0  32524  ffsrn  32652  difioo  32705  symgcom2  33041  eulerpartlemt  34362  fineqvac  35087  subfacp1lem1  35166  cvmscld  35260  mthmpps  35569  refssfne  36346  topjoin  36353  pibt2  37405  poimirlem3  37617  poimirlem28  37642  rntrclfvOAI  42679  istopclsd  42688  nacsfix  42700  diophrw  42747  tfsconcatb0  43333  onsucunipr  43361  oaun3  43371  clcnvlem  43612  cnvrcl0  43614  dmtrcl  43616  rntrcl  43617  iunrelexp0  43691  dmtrclfvRP  43719  rntrclfv  43721  cotrclrcl  43731  clsk3nimkb  44029  limciccioolb  45619  limcicciooub  45635  ioccncflimc  45883  icocncflimc  45887  stoweidlem44  46042  dirkercncflem3  46103  fourierdlem62  46166  ismeannd  46465  cycl3grtri  47946