Theorem ssequn2 4141

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 4138	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		uncom 4111	. . 3 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	2	eqeq1i 2766	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
4	1, 3	bitri 277	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)

Syntax hints:   ↔ wb 208   = wceq 1559   ∪ cun 3902   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-ss 3921

This theorem is referenced by:  unabs  4217  undifr  4436  tppreqb  4764  pwssun  5537  cnvimassrndm  6134  relresfld  6259  ordssun  6446  ordequn  6447  onunel  6449  onun2  6452  oneluni  6462  fsnunf  7165  sorpssun  7709  ordunpr  7802  omun  7864  fodomr  9096  unfi  9135  enp1ilem  9218  pwfilem  9258  fodomfir  9268  brwdom2  9518  sucprcreg  9551  sucprcregOLD  9552  dfacfin7  10353  hashbclem  14462  incexclem  15849  ramub1lem1  17045  ramub1lem2  17046  mreexmrid  17658  lspun0  21058  lbsextlem4  21211  cldlp  23190  ordtuni  23230  lfinun  23565  cldsubg  24151  trust  24269  nulmbl2  25578  limcmpt2  25926  cnplimc  25929  dvreslem  25951  dvaddbr  25980  dvmulbr  25981  lhop  26058  plypf1  26252  coeeulem  26264  coeeu  26265  coef2  26271  rlimcnp  27007  noetalem1  27782  addsproplem2  28040  ex-un  30572  shs0i  31598  chj0i  31604  disjun0  32744  ffsrn  32880  difioo  32934  symgcom2  33225  eulerpartlemt  34629  fineqvac  35376  subfacp1lem1  35493  cvmscld  35587  mthmpps  35896  refssfne  36682  topjoin  36689  pibt2  37875  poimirlem3  38086  poimirlem28  38111  rntrclfvOAI  43236  istopclsd  43245  nacsfix  43257  diophrw  43304  tfsconcatb0  43885  onsucunipr  43913  oaun3  43923  clcnvlem  44163  cnvrcl0  44165  dmtrcl  44167  rntrcl  44168  iunrelexp0  44242  dmtrclfvRP  44270  rntrclfv  44272  cotrclrcl  44282  clsk3nimkb  44580  limciccioolb  46161  limcicciooub  46175  ioccncflimc  46423  icocncflimc  46427  stoweidlem44  46582  dirkercncflem3  46643  fourierdlem62  46706  ismeannd  47005  cycl3grtri  48533