Theorem ssequn2 4182

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

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

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 3952  df-in 3954  df-ss 3964

This theorem is referenced by:  unabs  4253  undifr  4481  tppreqb  4807  pwssun  5570  cnvimassrndm  6148  relresfld  6272  ordssun  6463  ordequn  6464  onunel  6466  onun2  6469  oneluni  6480  fsnunf  7178  sorpssun  7715  ordunpr  7809  omun  7873  fodomr  9124  unfi  9168  pwfilem  9173  enp1ilem  9274  pwfilemOLD  9342  brwdom2  9564  sucprcreg  9592  dfacfin7  10390  hashbclem  14407  incexclem  15778  ramub1lem1  16955  ramub1lem2  16956  mreexmrid  17583  lspun0  20610  lbsextlem4  20762  cldlp  22636  ordtuni  22676  lfinun  23011  cldsubg  23597  trust  23716  nulmbl2  25035  limcmpt2  25383  cnplimc  25386  dvreslem  25408  dvaddbr  25437  dvmulbr  25438  lhop  25515  plypf1  25708  coeeulem  25720  coeeu  25721  coef2  25727  rlimcnp  26450  noetalem1  27224  addsproplem2  27434  ex-un  29657  shs0i  30680  chj0i  30686  disjun0  31804  ffsrn  31932  difioo  31971  symgcom2  32223  eulerpartlemt  33308  fineqvac  34035  subfacp1lem1  34108  cvmscld  34202  mthmpps  34511  gg-dvmulbr  35113  refssfne  35181  topjoin  35188  pibt2  36236  poimirlem3  36429  poimirlem28  36454  rntrclfvOAI  41362  istopclsd  41371  nacsfix  41383  diophrw  41430  tfsconcatb0  42027  onsucunipr  42055  oaun3  42065  clcnvlem  42307  cnvrcl0  42309  dmtrcl  42311  rntrcl  42312  iunrelexp0  42386  dmtrclfvRP  42414  rntrclfv  42416  cotrclrcl  42426  clsk3nimkb  42724  limciccioolb  44272  limcicciooub  44288  ioccncflimc  44536  icocncflimc  44540  stoweidlem44  44695  dirkercncflem3  44756  fourierdlem62  44819  ismeannd  45118