Theorem ssequn2 4184

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

Syntax hints:   ↔ wb 205   = wceq 1542   ∪ cun 3947   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966

This theorem is referenced by:  unabs  4255  undifr  4483  tppreqb  4809  pwssun  5572  cnvimassrndm  6152  relresfld  6276  ordssun  6467  ordequn  6468  onunel  6470  onun2  6473  oneluni  6484  fsnunf  7183  sorpssun  7720  ordunpr  7814  omun  7878  fodomr  9128  unfi  9172  pwfilem  9177  enp1ilem  9278  pwfilemOLD  9346  brwdom2  9568  sucprcreg  9596  dfacfin7  10394  hashbclem  14411  incexclem  15782  ramub1lem1  16959  ramub1lem2  16960  mreexmrid  17587  lspun0  20622  lbsextlem4  20774  cldlp  22654  ordtuni  22694  lfinun  23029  cldsubg  23615  trust  23734  nulmbl2  25053  limcmpt2  25401  cnplimc  25404  dvreslem  25426  dvaddbr  25455  dvmulbr  25456  lhop  25533  plypf1  25726  coeeulem  25738  coeeu  25739  coef2  25745  rlimcnp  26470  noetalem1  27244  addsproplem2  27454  ex-un  29677  shs0i  30702  chj0i  30708  disjun0  31826  ffsrn  31954  difioo  31993  symgcom2  32245  eulerpartlemt  33370  fineqvac  34097  subfacp1lem1  34170  cvmscld  34264  mthmpps  34573  gg-dvmulbr  35175  refssfne  35243  topjoin  35250  pibt2  36298  poimirlem3  36491  poimirlem28  36516  rntrclfvOAI  41429  istopclsd  41438  nacsfix  41450  diophrw  41497  tfsconcatb0  42094  onsucunipr  42122  oaun3  42132  clcnvlem  42374  cnvrcl0  42376  dmtrcl  42378  rntrcl  42379  iunrelexp0  42453  dmtrclfvRP  42481  rntrclfv  42483  cotrclrcl  42493  clsk3nimkb  42791  limciccioolb  44337  limcicciooub  44353  ioccncflimc  44601  icocncflimc  44605  stoweidlem44  44760  dirkercncflem3  44821  fourierdlem62  44884  ismeannd  45183