Theorem ssequn2 4125

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 4122	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		uncom 4095	. . 3 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	2	eqeq1i 2745	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
4	1, 3	bitri 276	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)

Syntax hints:   ↔ wb 207   = wceq 1547   ∪ cun 3888   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907

This theorem is referenced by:  unabs  4200  undifr  4418  tppreqb  4745  pwssun  5517  cnvimassrndm  6110  relresfld  6234  ordssun  6421  ordequn  6422  onunel  6424  onun2  6427  oneluni  6437  fsnunf  7136  sorpssun  7680  ordunpr  7773  omun  7835  fodomr  9063  unfi  9102  enp1ilem  9185  pwfilem  9225  fodomfir  9235  brwdom2  9485  sucprcreg  9518  sucprcregOLD  9519  dfacfin7  10319  hashbclem  14412  incexclem  15799  ramub1lem1  16995  ramub1lem2  16996  mreexmrid  17607  lspun0  21008  lbsextlem4  21161  cldlp  23140  ordtuni  23180  lfinun  23515  cldsubg  24101  trust  24219  nulmbl2  25528  limcmpt2  25876  cnplimc  25879  dvreslem  25901  dvaddbr  25930  dvmulbr  25931  lhop  26008  plypf1  26202  coeeulem  26214  coeeu  26215  coef2  26221  rlimcnp  26954  noetalem1  27730  addsproplem2  27987  ex-un  30519  shs0i  31545  chj0i  31551  disjun0  32691  ffsrn  32827  difioo  32881  symgcom2  33172  eulerpartlemt  34562  fineqvac  35304  subfacp1lem1  35414  cvmscld  35508  mthmpps  35817  refssfne  36593  topjoin  36600  pibt2  37786  poimirlem3  37997  poimirlem28  38022  rntrclfvOAI  43147  istopclsd  43156  nacsfix  43168  diophrw  43215  tfsconcatb0  43796  onsucunipr  43824  oaun3  43834  clcnvlem  44074  cnvrcl0  44076  dmtrcl  44078  rntrcl  44079  iunrelexp0  44153  dmtrclfvRP  44181  rntrclfv  44183  cotrclrcl  44193  clsk3nimkb  44491  limciccioolb  46073  limcicciooub  46087  ioccncflimc  46335  icocncflimc  46339  stoweidlem44  46494  dirkercncflem3  46555  fourierdlem62  46618  ismeannd  46917  cycl3grtri  48445