Theorem ssequn2 4139

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∪ cun 3900   ⊆ wss 3902

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-ss 3919

This theorem is referenced by:  unabs  4215  undifr  4433  tppreqb  4757  pwssun  5508  cnvimassrndm  6099  relresfld  6223  ordssun  6410  ordequn  6411  onunel  6413  onun2  6416  oneluni  6426  fsnunf  7119  sorpssun  7663  ordunpr  7756  omun  7818  fodomr  9041  unfi  9080  enp1ilem  9162  pwfilem  9202  fodomfir  9212  brwdom2  9459  sucprcreg  9490  dfacfin7  10287  hashbclem  14356  incexclem  15740  ramub1lem1  16935  ramub1lem2  16936  mreexmrid  17546  lspun0  20942  lbsextlem4  21096  cldlp  23063  ordtuni  23103  lfinun  23438  cldsubg  24024  trust  24142  nulmbl2  25462  limcmpt2  25810  cnplimc  25813  dvreslem  25835  dvaddbr  25865  dvmulbr  25866  dvmulbrOLD  25867  lhop  25946  plypf1  26142  coeeulem  26154  coeeu  26155  coef2  26161  rlimcnp  26900  noetalem1  27678  addsproplem2  27911  ex-un  30399  shs0i  31424  chj0i  31430  disjun0  32570  ffsrn  32706  difioo  32760  symgcom2  33048  eulerpartlemt  34379  fineqvac  35127  subfacp1lem1  35211  cvmscld  35305  mthmpps  35614  refssfne  36391  topjoin  36398  pibt2  37450  poimirlem3  37662  poimirlem28  37687  rntrclfvOAI  42723  istopclsd  42732  nacsfix  42744  diophrw  42791  tfsconcatb0  43376  onsucunipr  43404  oaun3  43414  clcnvlem  43655  cnvrcl0  43657  dmtrcl  43659  rntrcl  43660  iunrelexp0  43734  dmtrclfvRP  43762  rntrclfv  43764  cotrclrcl  43774  clsk3nimkb  44072  limciccioolb  45660  limcicciooub  45674  ioccncflimc  45922  icocncflimc  45926  stoweidlem44  46081  dirkercncflem3  46142  fourierdlem62  46205  ismeannd  46504  cycl3grtri  47977