Theorem ssequn2 4110

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

Syntax hints:   ↔ wb 209   = wceq 1538   ∪ cun 3879   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898

This theorem is referenced by:  unabs  4181  tppreqb  4698  pwssun  5421  pwundifOLD  5422  relresfld  6095  ordssun  6258  ordequn  6259  oneluni  6271  fsnunf  6924  sorpssun  7436  ordunpr  7521  fodomr  8652  enp1ilem  8736  pwfilem  8802  brwdom2  9021  sucprcreg  9049  dfacfin7  9810  hashbclem  13806  incexclem  15183  ramub1lem1  16352  ramub1lem2  16353  mreexmrid  16906  lspun0  19776  lbsextlem4  19926  cldlp  21755  ordtuni  21795  lfinun  22130  cldsubg  22716  trust  22835  nulmbl2  24140  limcmpt2  24487  cnplimc  24490  dvreslem  24512  dvaddbr  24541  dvmulbr  24542  lhop  24619  plypf1  24809  coeeulem  24821  coeeu  24822  coef2  24828  rlimcnp  25551  ex-un  28209  shs0i  29232  chj0i  29238  disjun0  30358  ffsrn  30491  difioo  30531  symgcom2  30778  eulerpartlemt  31739  subfacp1lem1  32539  cvmscld  32633  mthmpps  32942  refssfne  33819  topjoin  33826  pibt2  34834  poimirlem3  35060  poimirlem28  35085  rntrclfvOAI  39632  istopclsd  39641  nacsfix  39653  diophrw  39700  clcnvlem  40323  cnvrcl0  40325  dmtrcl  40327  rntrcl  40328  iunrelexp0  40403  dmtrclfvRP  40431  rntrclfv  40433  cotrclrcl  40443  clsk3nimkb  40743  limciccioolb  42263  limcicciooub  42279  ioccncflimc  42527  icocncflimc  42531  stoweidlem44  42686  dirkercncflem3  42747  fourierdlem62  42810  ismeannd  43106