Theorem ssequn2 4138

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∪ cun 3896   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-ss 3915

This theorem is referenced by:  unabs  4214  undifr  4432  tppreqb  4756  pwssun  5511  cnvimassrndm  6104  relresfld  6228  ordssun  6415  ordequn  6416  onunel  6418  onun2  6421  oneluni  6431  fsnunf  7125  sorpssun  7669  ordunpr  7762  omun  7824  fodomr  9048  unfi  9087  enp1ilem  9169  pwfilem  9209  fodomfir  9219  brwdom2  9466  sucprcreg  9497  dfacfin7  10297  hashbclem  14361  incexclem  15745  ramub1lem1  16940  ramub1lem2  16941  mreexmrid  17551  lspun0  20946  lbsextlem4  21100  cldlp  23066  ordtuni  23106  lfinun  23441  cldsubg  24027  trust  24145  nulmbl2  25465  limcmpt2  25813  cnplimc  25816  dvreslem  25838  dvaddbr  25868  dvmulbr  25869  dvmulbrOLD  25870  lhop  25949  plypf1  26145  coeeulem  26157  coeeu  26158  coef2  26164  rlimcnp  26903  noetalem1  27681  addsproplem2  27914  ex-un  30406  shs0i  31431  chj0i  31437  disjun0  32577  ffsrn  32715  difioo  32769  symgcom2  33060  eulerpartlemt  34405  fineqvac  35160  subfacp1lem1  35244  cvmscld  35338  mthmpps  35647  refssfne  36423  topjoin  36430  pibt2  37482  poimirlem3  37683  poimirlem28  37708  rntrclfvOAI  42808  istopclsd  42817  nacsfix  42829  diophrw  42876  tfsconcatb0  43461  onsucunipr  43489  oaun3  43499  clcnvlem  43740  cnvrcl0  43742  dmtrcl  43744  rntrcl  43745  iunrelexp0  43819  dmtrclfvRP  43847  rntrclfv  43849  cotrclrcl  43859  clsk3nimkb  44157  limciccioolb  45745  limcicciooub  45759  ioccncflimc  46007  icocncflimc  46011  stoweidlem44  46166  dirkercncflem3  46227  fourierdlem62  46290  ismeannd  46589  cycl3grtri  48071