Theorem ssequn2 4013

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 4010	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		uncom 3984	. . 3 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	2	eqeq1i 2830	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
4	1, 3	bitri 267	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)

Syntax hints:   ↔ wb 198   = wceq 1658   ∪ cun 3796   ⊆ wss 3798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-v 3416  df-un 3803  df-in 3805  df-ss 3812

This theorem is referenced by:  unabs  4084  tppreqb  4554  pwssun  5246  pwundif  5247  relresfld  5903  ordssun  6062  ordequn  6063  oneluni  6075  fsnunf  6707  sorpssun  7204  ordunpr  7287  fodomr  8380  enp1ilem  8463  pwfilem  8529  brwdom2  8747  sucprcreg  8775  dfacfin7  9536  hashbclem  13525  incexclem  14942  ramub1lem1  16101  ramub1lem2  16102  mreexmrid  16656  lspun0  19370  lbsextlem4  19522  cldlp  21325  ordtuni  21365  lfinun  21699  cldsubg  22284  trust  22403  nulmbl2  23702  limcmpt2  24047  cnplimc  24050  dvreslem  24072  dvaddbr  24100  dvmulbr  24101  lhop  24178  plypf1  24367  coeeulem  24379  coeeu  24380  coef2  24386  rlimcnp  25105  ex-un  27839  shs0i  28863  chj0i  28869  disjun0  29955  ffsrn  30052  difioo  30091  eulerpartlemt  30978  subfacp1lem1  31707  cvmscld  31801  mthmpps  32025  refssfne  32891  topjoin  32898  poimirlem3  33956  poimirlem28  33981  rntrclfvOAI  38098  istopclsd  38107  nacsfix  38119  diophrw  38166  clcnvlem  38771  cnvrcl0  38773  dmtrcl  38775  rntrcl  38776  iunrelexp0  38835  dmtrclfvRP  38863  rntrclfv  38865  cotrclrcl  38875  clsk3nimkb  39178  limciccioolb  40648  limcicciooub  40664  ioccncflimc  40893  icocncflimc  40897  stoweidlem44  41055  dirkercncflem3  41116  fourierdlem62  41179  ismeannd  41475