Theorem ssequn2 4129

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∪ cun 3887   ⊆ wss 3889

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906

This theorem is referenced by:  unabs  4205  undifr  4423  tppreqb  4750  pwssun  5523  cnvimassrndm  6116  relresfld  6240  ordssun  6427  ordequn  6428  onunel  6430  onun2  6433  oneluni  6443  fsnunf  7140  sorpssun  7684  ordunpr  7777  omun  7839  fodomr  9066  unfi  9105  enp1ilem  9188  pwfilem  9228  fodomfir  9238  brwdom2  9488  sucprcreg  9520  sucprcregOLD  9521  dfacfin7  10321  hashbclem  14414  incexclem  15801  ramub1lem1  16997  ramub1lem2  16998  mreexmrid  17609  lspun0  21006  lbsextlem4  21159  cldlp  23115  ordtuni  23155  lfinun  23490  cldsubg  24076  trust  24194  nulmbl2  25503  limcmpt2  25851  cnplimc  25854  dvreslem  25876  dvaddbr  25905  dvmulbr  25906  lhop  25983  plypf1  26177  coeeulem  26189  coeeu  26190  coef2  26196  rlimcnp  26929  noetalem1  27705  addsproplem2  27962  ex-un  30494  shs0i  31520  chj0i  31526  disjun0  32665  ffsrn  32801  difioo  32855  symgcom2  33145  eulerpartlemt  34515  fineqvac  35260  subfacp1lem1  35361  cvmscld  35455  mthmpps  35764  refssfne  36540  topjoin  36547  pibt2  37733  poimirlem3  37944  poimirlem28  37969  rntrclfvOAI  43123  istopclsd  43132  nacsfix  43144  diophrw  43191  tfsconcatb0  43772  onsucunipr  43800  oaun3  43810  clcnvlem  44050  cnvrcl0  44052  dmtrcl  44054  rntrcl  44055  iunrelexp0  44129  dmtrclfvRP  44157  rntrclfv  44159  cotrclrcl  44169  clsk3nimkb  44467  limciccioolb  46051  limcicciooub  46065  ioccncflimc  46313  icocncflimc  46317  stoweidlem44  46472  dirkercncflem3  46533  fourierdlem62  46596  ismeannd  46895  cycl3grtri  48423