Theorem ssequn2 4135

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∪ cun 3897   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916

This theorem is used by:  unabs  4211  undifr  4439  tppreqb  4768  pwssun  5543  cnvimassrndm  6141  relresfldOLD  6272  ordssun  6460  ordequn  6461  onunel  6463  onun2  6466  oneluni  6476  fsnunf  7182  sorpssun  7735  ordunpr  7826  omun  7888  fodomr  9131  unfi  9170  enp1ilem  9253  pwfilem  9293  fodomfir  9303  brwdom2  9551  sucprcreg  9584  sucprcregOLD  9585  dfacfin7  10458  hashbclem  14577  incexclem  15985  ramub1lem1  17184  ramub1lem2  17185  mreexmrid  17797  lspun0  21266  lbsextlem4  21419  cldlp  23448  ordtuni  23488  lfinun  23824  cldsubg  24410  trust  24528  nulmbl2  25837  limcmpt2  26184  cnplimc  26187  dvreslem  26209  dvaddbr  26238  dvmulbr  26239  lhop  26316  plypf1  26511  coeeulem  26523  coeeu  26524  coef2  26530  rlimcnp  27275  noetalem1  28080  addsproplem2  28338  ex-un  31007  shs0i  32033  chj0i  32039  disjun0  33171  ffsrn  33302  difioo  33356  symgcom2  33627  eulerpartlemt  34986  fineqvac  35757  subfacp1lem1  35913  cvmscld  36007  mthmpps  36316  refssfne  37116  topjoin  37123  pibt2  38308  poimirlem3  38509  poimirlem28  38534  rntrclfvOAI  43655  istopclsd  43664  nacsfix  43676  diophrw  43723  tfsconcatb0  44304  onsucunipr  44332  oaun3  44342  clcnvlem  44582  cnvrcl0  44584  dmtrcl  44586  rntrcl  44587  iunrelexp0  44661  dmtrclfvRP  44689  rntrclfv  44691  cotrclrcl  44701  clsk3nimkb  44999  limciccioolb  46577  limcicciooub  46591  ioccncflimc  46839  icocncflimc  46843  stoweidlem44  46998  dirkercncflem3  47059  fourierdlem62  47122  ismeannd  47421  cycl3grtri  48989