Theorem ssequn2 4212

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

Syntax hints:   ↔ wb 206   = wceq 1537   ∪ cun 3974   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993

This theorem is referenced by:  unabs  4284  undifr  4506  tppreqb  4830  pwssun  5590  cnvimassrndm  6183  relresfld  6307  ordssun  6497  ordequn  6498  onunel  6500  onun2  6503  oneluni  6514  fsnunf  7219  sorpssun  7765  ordunpr  7862  omun  7926  fodomr  9194  unfi  9238  enp1ilem  9340  pwfilem  9384  fodomfir  9396  pwfilemOLD  9416  brwdom2  9642  sucprcreg  9670  dfacfin7  10468  hashbclem  14501  incexclem  15884  ramub1lem1  17073  ramub1lem2  17074  mreexmrid  17701  lspun0  21032  lbsextlem4  21186  cldlp  23179  ordtuni  23219  lfinun  23554  cldsubg  24140  trust  24259  nulmbl2  25590  limcmpt2  25939  cnplimc  25942  dvreslem  25964  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  lhop  26075  plypf1  26271  coeeulem  26283  coeeu  26284  coef2  26290  rlimcnp  27026  noetalem1  27804  addsproplem2  28021  ex-un  30456  shs0i  31481  chj0i  31487  disjun0  32617  ffsrn  32743  difioo  32787  symgcom2  33077  eulerpartlemt  34336  fineqvac  35073  subfacp1lem1  35147  cvmscld  35241  mthmpps  35550  refssfne  36324  topjoin  36331  pibt2  37383  poimirlem3  37583  poimirlem28  37608  rntrclfvOAI  42647  istopclsd  42656  nacsfix  42668  diophrw  42715  tfsconcatb0  43306  onsucunipr  43334  oaun3  43344  clcnvlem  43585  cnvrcl0  43587  dmtrcl  43589  rntrcl  43590  iunrelexp0  43664  dmtrclfvRP  43692  rntrclfv  43694  cotrclrcl  43704  clsk3nimkb  44002  limciccioolb  45542  limcicciooub  45558  ioccncflimc  45806  icocncflimc  45810  stoweidlem44  45965  dirkercncflem3  46026  fourierdlem62  46089  ismeannd  46388