Theorem ssequn2 4143

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

Syntax hints:   ↔ wb 209   = wceq 1570   ∪ cun 3904   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923

This theorem is referenced by:  unabs  4219  undifr  4445  tppreqb  4774  pwssun  5555  cnvimassrndm  6151  relresfld  6279  ordssun  6467  ordequn  6468  onunel  6470  onun2  6473  oneluni  6483  fsnunf  7185  sorpssun  7729  ordunpr  7823  omun  7885  fodomr  9117  unfi  9156  enp1ilem  9239  pwfilem  9278  fodomfir  9288  brwdom2  9536  sucprcreg  9569  sucprcregOLD  9570  dfacfin7  10384  hashbclem  14491  incexclem  15892  ramub1lem1  17087  ramub1lem2  17088  mreexmrid  17700  lspun0  21113  lbsextlem4  21266  cldlp  23288  ordtuni  23328  lfinun  23663  cldsubg  24249  trust  24367  nulmbl2  25676  limcmpt2  26024  cnplimc  26027  dvreslem  26049  dvaddbr  26078  dvmulbr  26079  lhop  26156  plypf1  26350  coeeulem  26362  coeeu  26363  coef2  26369  rlimcnp  27108  noetalem1  27883  addsproplem2  28141  ex-un  30753  shs0i  31779  chj0i  31785  disjun0  32918  ffsrn  33051  difioo  33105  symgcom2  33382  eulerpartlemt  34739  fineqvac  35507  subfacp1lem1  35649  cvmscld  35743  mthmpps  36052  refssfne  36847  topjoin  36854  pibt2  38041  poimirlem3  38252  poimirlem28  38277  rntrclfvOAI  43402  istopclsd  43411  nacsfix  43423  diophrw  43470  tfsconcatb0  44051  onsucunipr  44079  oaun3  44089  clcnvlem  44329  cnvrcl0  44331  dmtrcl  44333  rntrcl  44334  iunrelexp0  44408  dmtrclfvRP  44436  rntrclfv  44438  cotrclrcl  44448  clsk3nimkb  44746  limciccioolb  46317  limcicciooub  46331  ioccncflimc  46579  icocncflimc  46583  stoweidlem44  46738  dirkercncflem3  46799  fourierdlem62  46862  ismeannd  47161  cycl3grtri  48689