Theorem ssequn2 4162

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

Syntax hints:   ↔ wb 208   = wceq 1536   ∪ cun 3937   ⊆ wss 3939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-v 3499  df-un 3944  df-in 3946  df-ss 3955

This theorem is referenced by:  unabs  4234  tppreqb  4741  pwssun  5459  pwundifOLD  5460  relresfld  6130  ordssun  6293  ordequn  6294  oneluni  6306  fsnunf  6950  sorpssun  7459  ordunpr  7544  fodomr  8671  enp1ilem  8755  pwfilem  8821  brwdom2  9040  sucprcreg  9068  dfacfin7  9824  hashbclem  13813  incexclem  15194  ramub1lem1  16365  ramub1lem2  16366  mreexmrid  16917  lspun0  19786  lbsextlem4  19936  cldlp  21761  ordtuni  21801  lfinun  22136  cldsubg  22722  trust  22841  nulmbl2  24140  limcmpt2  24485  cnplimc  24488  dvreslem  24510  dvaddbr  24538  dvmulbr  24539  lhop  24616  plypf1  24805  coeeulem  24817  coeeu  24818  coef2  24824  rlimcnp  25546  ex-un  28206  shs0i  29229  chj0i  29235  disjun0  30348  ffsrn  30468  difioo  30508  symgcom2  30732  eulerpartlemt  31633  subfacp1lem1  32430  cvmscld  32524  mthmpps  32833  refssfne  33710  topjoin  33717  pibt2  34702  poimirlem3  34899  poimirlem28  34924  rntrclfvOAI  39294  istopclsd  39303  nacsfix  39315  diophrw  39362  clcnvlem  39989  cnvrcl0  39991  dmtrcl  39993  rntrcl  39994  iunrelexp0  40053  dmtrclfvRP  40081  rntrclfv  40083  cotrclrcl  40093  clsk3nimkb  40396  limciccioolb  41908  limcicciooub  41924  ioccncflimc  42174  icocncflimc  42178  stoweidlem44  42336  dirkercncflem3  42397  fourierdlem62  42460  ismeannd  42756