Theorem ssequn2 3786

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

Syntax hints:   ↔ wb 196   = wceq 1483   ∪ cun 3572   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588

This theorem is referenced by:  unabs  3854  tppreqb  4336  pwssun  5020  pwundif  5021  relresfld  5662  ordssun  5827  ordequn  5828  oneluni  5840  fsnunf  6451  sorpssun  6944  ordunpr  7026  fodomr  8111  enp1ilem  8194  pwfilem  8260  brwdom2  8478  sucprcreg  8506  dfacfin7  9221  hashbclem  13236  incexclem  14568  ramub1lem1  15730  ramub1lem2  15731  mreexmrid  16303  lspun0  19011  lbsextlem4  19161  cldlp  20954  ordtuni  20994  lfinun  21328  cldsubg  21914  trust  22033  nulmbl2  23304  limcmpt2  23648  cnplimc  23651  dvreslem  23673  dvaddbr  23701  dvmulbr  23702  lhop  23779  plypf1  23968  coeeulem  23980  coeeu  23981  coef2  23987  rlimcnp  24692  ex-un  27281  shs0i  28308  chj0i  28314  disjun0  29408  ffsrn  29504  difioo  29544  eulerpartlemt  30433  subfacp1lem1  31161  cvmscld  31255  mthmpps  31479  refssfne  32353  topjoin  32360  poimirlem3  33412  poimirlem28  33437  rntrclfvOAI  37254  istopclsd  37263  nacsfix  37275  diophrw  37322  clcnvlem  37930  cnvrcl0  37932  dmtrcl  37934  rntrcl  37935  iunrelexp0  37994  dmtrclfvRP  38022  rntrclfv  38024  cotrclrcl  38034  clsk3nimkb  38338  limciccioolb  39853  limcicciooub  39869  ioccncflimc  40098  icocncflimc  40102  stoweidlem44  40261  dirkercncflem3  40322  fourierdlem62  40385  ismeannd  40684