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

Syntax hints:   ↔ wb 206   = wceq 1541   ∪ cun 3899   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918

This theorem is referenced by:  unabs  4217  undifr  4435  tppreqb  4761  pwssun  5516  cnvimassrndm  6110  relresfld  6234  ordssun  6421  ordequn  6422  onunel  6424  onun2  6427  oneluni  6437  fsnunf  7131  sorpssun  7675  ordunpr  7768  omun  7830  fodomr  9056  unfi  9095  enp1ilem  9178  pwfilem  9218  fodomfir  9228  brwdom2  9478  sucprcreg  9509  dfacfin7  10309  hashbclem  14375  incexclem  15759  ramub1lem1  16954  ramub1lem2  16955  mreexmrid  17566  lspun0  20962  lbsextlem4  21116  cldlp  23094  ordtuni  23134  lfinun  23469  cldsubg  24055  trust  24173  nulmbl2  25493  limcmpt2  25841  cnplimc  25844  dvreslem  25866  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  lhop  25977  plypf1  26173  coeeulem  26185  coeeu  26186  coef2  26192  rlimcnp  26931  noetalem1  27709  addsproplem2  27966  ex-un  30499  shs0i  31524  chj0i  31530  disjun0  32670  ffsrn  32807  difioo  32862  symgcom2  33166  eulerpartlemt  34528  fineqvac  35272  subfacp1lem1  35373  cvmscld  35467  mthmpps  35776  refssfne  36552  topjoin  36559  pibt2  37618  poimirlem3  37820  poimirlem28  37845  rntrclfvOAI  42929  istopclsd  42938  nacsfix  42950  diophrw  42997  tfsconcatb0  43582  onsucunipr  43610  oaun3  43620  clcnvlem  43860  cnvrcl0  43862  dmtrcl  43864  rntrcl  43865  iunrelexp0  43939  dmtrclfvRP  43967  rntrclfv  43969  cotrclrcl  43979  clsk3nimkb  44277  limciccioolb  45863  limcicciooub  45877  ioccncflimc  46125  icocncflimc  46129  stoweidlem44  46284  dirkercncflem3  46345  fourierdlem62  46408  ismeannd  46707  cycl3grtri  48189