Theorem ssequn2 4187

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ⊆ wss 3895   ∪ cun 4149

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151

This theorem is used by:  unabs  4210  undifr  4438  tppreqb  4764  pwssun  5542  cnvimassrndmOLD  6199  imadifssrn  6201  relresfldOLD  6279  ordssun  6467  ordequn  6468  onunel  6470  onun2  6473  oneluni  6483  fsnunf  7190  sorpssun  7746  ordunpr  7837  omun  7899  fodomr  9150  unfi  9189  enp1ilem  9272  pwfilem  9312  fodomfir  9322  brwdom2  9570  sucprcreg  9603  sucprcregOLD  9604  dfacfin7  10480  hashbclem  14600  incexclem  16010  ramub1lem1  17209  ramub1lem2  17210  mreexmrid  17822  lspun0  21291  lbsextlem4  21444  cldlp  23473  ordtuni  23513  lfinun  23849  cldsubg  24435  trust  24553  nulmbl2  25862  limcmpt2  26209  cnplimc  26212  dvreslem  26234  dvaddbr  26263  dvmulbr  26264  lhop  26341  plypf1  26536  coeeulem  26548  coeeu  26549  coef2  26555  rlimcnp  27298  noetalem1  28103  addsproplem2  28361  ex-un  31030  shs0i  32056  chj0i  32062  disjun0  33236  ffsrn  33366  difioo  33420  symgcom2  33691  eulerpartlemt  35049  ordunmax  35765  fineqvac  35840  subfacp1lem1  36030  cvmscld  36124  mthmpps  36433  refssfne  37238  topjoin  37245  pibt2  38433  poimirlem3  38634  poimirlem28  38659  rntrclfvOAI  43795  istopclsd  43804  nacsfix  43816  diophrw  43863  tfsconcatb0  44439  onsucunipr  44467  oaun3  44477  clcnvlem  44716  cnvrcl0  44718  dmtrcl  44720  rntrcl  44721  iunrelexp0  44795  dmtrclfvRP  44823  rntrclfv  44825  cotrclrcl  44835  clsk3nimkb  45133  limciccioolb  46726  limcicciooub  46740  ioccncflimc  46988  icocncflimc  46992  stoweidlem44  47147  dirkercncflem3  47208  fourierdlem62  47271  ismeannd  47570  cycl3grtri  49138