Theorem ssequn2 4142

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∪ cun 3903   ⊆ wss 3905

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 3440  df-un 3910  df-ss 3922

This theorem is referenced by:  unabs  4218  undifr  4436  tppreqb  4759  pwssun  5515  cnvimassrndm  6105  relresfld  6228  ordssun  6415  ordequn  6416  onunel  6418  onun2  6421  oneluni  6431  fsnunf  7125  sorpssun  7670  ordunpr  7765  omun  7828  fodomr  9052  unfi  9095  enp1ilem  9181  pwfilem  9225  fodomfir  9237  brwdom2  9484  sucprcreg  9515  dfacfin7  10312  hashbclem  14377  incexclem  15761  ramub1lem1  16956  ramub1lem2  16957  mreexmrid  17567  lspun0  20932  lbsextlem4  21086  cldlp  23053  ordtuni  23093  lfinun  23428  cldsubg  24014  trust  24133  nulmbl2  25453  limcmpt2  25801  cnplimc  25804  dvreslem  25826  dvaddbr  25856  dvmulbr  25857  dvmulbrOLD  25858  lhop  25937  plypf1  26133  coeeulem  26145  coeeu  26146  coef2  26152  rlimcnp  26891  noetalem1  27669  addsproplem2  27900  ex-un  30386  shs0i  31411  chj0i  31417  disjun0  32557  ffsrn  32685  difioo  32738  symgcom2  33039  eulerpartlemt  34338  fineqvac  35071  subfacp1lem1  35151  cvmscld  35245  mthmpps  35554  refssfne  36331  topjoin  36338  pibt2  37390  poimirlem3  37602  poimirlem28  37627  rntrclfvOAI  42664  istopclsd  42673  nacsfix  42685  diophrw  42732  tfsconcatb0  43317  onsucunipr  43345  oaun3  43355  clcnvlem  43596  cnvrcl0  43598  dmtrcl  43600  rntrcl  43601  iunrelexp0  43675  dmtrclfvRP  43703  rntrclfv  43705  cotrclrcl  43715  clsk3nimkb  44013  limciccioolb  45603  limcicciooub  45619  ioccncflimc  45867  icocncflimc  45871  stoweidlem44  46026  dirkercncflem3  46087  fourierdlem62  46150  ismeannd  46449  cycl3grtri  47932