Theorem ssequn2 4113

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 4110	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		uncom 4083	. . 3 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	2	eqeq1i 2743	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
4	1, 3	bitri 274	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)

Syntax hints:   ↔ wb 205   = wceq 1539   ∪ cun 3881   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900

This theorem is referenced by:  unabs  4185  tppreqb  4735  pwssun  5476  pwundifOLD  5477  cnvimassrndm  6044  relresfld  6168  ordssun  6350  ordequn  6351  onun2  6355  oneluni  6364  fsnunf  7039  sorpssun  7561  ordunpr  7648  fodomr  8864  unfi  8917  pwfilem  8922  enp1ilem  8981  pwfilemOLD  9043  brwdom2  9262  sucprcreg  9290  dfacfin7  10086  hashbclem  14092  incexclem  15476  ramub1lem1  16655  ramub1lem2  16656  mreexmrid  17269  lspun0  20188  lbsextlem4  20338  cldlp  22209  ordtuni  22249  lfinun  22584  cldsubg  23170  trust  23289  nulmbl2  24605  limcmpt2  24953  cnplimc  24956  dvreslem  24978  dvaddbr  25007  dvmulbr  25008  lhop  25085  plypf1  25278  coeeulem  25290  coeeu  25291  coef2  25297  rlimcnp  26020  ex-un  28689  shs0i  29712  chj0i  29718  disjun0  30835  ffsrn  30966  difioo  31005  symgcom2  31255  eulerpartlemt  32238  fineqvac  32966  subfacp1lem1  33041  cvmscld  33135  mthmpps  33444  onunel  33592  noetalem1  33871  refssfne  34474  topjoin  34481  pibt2  35515  poimirlem3  35707  poimirlem28  35732  rntrclfvOAI  40429  istopclsd  40438  nacsfix  40450  diophrw  40497  clcnvlem  41120  cnvrcl0  41122  dmtrcl  41124  rntrcl  41125  iunrelexp0  41199  dmtrclfvRP  41227  rntrclfv  41229  cotrclrcl  41239  clsk3nimkb  41539  limciccioolb  43052  limcicciooub  43068  ioccncflimc  43316  icocncflimc  43320  stoweidlem44  43475  dirkercncflem3  43536  fourierdlem62  43599  ismeannd  43895