Theorem ssequn2 4189

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∪ cun 3949   ⊆ wss 3951

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 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968

This theorem is referenced by:  unabs  4265  undifr  4483  tppreqb  4805  pwssun  5575  cnvimassrndm  6172  relresfld  6296  ordssun  6486  ordequn  6487  onunel  6489  onun2  6492  oneluni  6503  fsnunf  7205  sorpssun  7750  ordunpr  7846  omun  7909  fodomr  9168  unfi  9211  enp1ilem  9312  pwfilem  9356  fodomfir  9368  brwdom2  9613  sucprcreg  9641  dfacfin7  10439  hashbclem  14491  incexclem  15872  ramub1lem1  17064  ramub1lem2  17065  mreexmrid  17686  lspun0  21009  lbsextlem4  21163  cldlp  23158  ordtuni  23198  lfinun  23533  cldsubg  24119  trust  24238  nulmbl2  25571  limcmpt2  25919  cnplimc  25922  dvreslem  25944  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  lhop  26055  plypf1  26251  coeeulem  26263  coeeu  26264  coef2  26270  rlimcnp  27008  noetalem1  27786  addsproplem2  28003  ex-un  30443  shs0i  31468  chj0i  31474  disjun0  32608  ffsrn  32740  difioo  32784  symgcom2  33104  eulerpartlemt  34373  fineqvac  35111  subfacp1lem1  35184  cvmscld  35278  mthmpps  35587  refssfne  36359  topjoin  36366  pibt2  37418  poimirlem3  37630  poimirlem28  37655  rntrclfvOAI  42702  istopclsd  42711  nacsfix  42723  diophrw  42770  tfsconcatb0  43357  onsucunipr  43385  oaun3  43395  clcnvlem  43636  cnvrcl0  43638  dmtrcl  43640  rntrcl  43641  iunrelexp0  43715  dmtrclfvRP  43743  rntrclfv  43745  cotrclrcl  43755  clsk3nimkb  44053  limciccioolb  45636  limcicciooub  45652  ioccncflimc  45900  icocncflimc  45904  stoweidlem44  46059  dirkercncflem3  46120  fourierdlem62  46183  ismeannd  46482  cycl3grtri  47914