Theorem ssequn2 3930

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 3927	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		uncom 3901	. . 3 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	2	eqeq1i 2766	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
4	1, 3	bitri 264	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)

Syntax hints:   ↔ wb 196   = wceq 1632   ∪ cun 3714   ⊆ wss 3716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-v 3343  df-un 3721  df-in 3723  df-ss 3730

This theorem is referenced by:  unabs  3998  tppreqb  4482  pwssun  5171  pwundif  5172  relresfld  5824  ordssun  5989  ordequn  5990  oneluni  6002  fsnunf  6617  sorpssun  7111  ordunpr  7193  fodomr  8279  enp1ilem  8362  pwfilem  8428  brwdom2  8646  sucprcreg  8674  dfacfin7  9434  hashbclem  13449  incexclem  14788  ramub1lem1  15953  ramub1lem2  15954  mreexmrid  16526  lspun0  19234  lbsextlem4  19384  cldlp  21177  ordtuni  21217  lfinun  21551  cldsubg  22136  trust  22255  nulmbl2  23525  limcmpt2  23868  cnplimc  23871  dvreslem  23893  dvaddbr  23921  dvmulbr  23922  lhop  23999  plypf1  24188  coeeulem  24200  coeeu  24201  coef2  24207  rlimcnp  24913  ex-un  27614  shs0i  28639  chj0i  28645  disjun0  29737  ffsrn  29835  difioo  29875  eulerpartlemt  30764  subfacp1lem1  31490  cvmscld  31584  mthmpps  31808  refssfne  32681  topjoin  32688  poimirlem3  33744  poimirlem28  33769  rntrclfvOAI  37775  istopclsd  37784  nacsfix  37796  diophrw  37843  clcnvlem  38451  cnvrcl0  38453  dmtrcl  38455  rntrcl  38456  iunrelexp0  38515  dmtrclfvRP  38543  rntrclfv  38545  cotrclrcl  38555  clsk3nimkb  38859  limciccioolb  40375  limcicciooub  40391  ioccncflimc  40620  icocncflimc  40624  stoweidlem44  40783  dirkercncflem3  40844  fourierdlem62  40907  ismeannd  41206