Theorem ssequn2 4164

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∪ cun 3924   ⊆ wss 3926

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-ss 3943

This theorem is referenced by:  unabs  4240  undifr  4458  tppreqb  4781  pwssun  5545  cnvimassrndm  6141  relresfld  6265  ordssun  6456  ordequn  6457  onunel  6459  onun2  6462  oneluni  6473  fsnunf  7177  sorpssun  7724  ordunpr  7820  omun  7883  fodomr  9142  unfi  9185  enp1ilem  9284  pwfilem  9328  fodomfir  9340  brwdom2  9587  sucprcreg  9615  dfacfin7  10413  hashbclem  14470  incexclem  15852  ramub1lem1  17046  ramub1lem2  17047  mreexmrid  17655  lspun0  20968  lbsextlem4  21122  cldlp  23088  ordtuni  23128  lfinun  23463  cldsubg  24049  trust  24168  nulmbl2  25489  limcmpt2  25837  cnplimc  25840  dvreslem  25862  dvaddbr  25892  dvmulbr  25893  dvmulbrOLD  25894  lhop  25973  plypf1  26169  coeeulem  26181  coeeu  26182  coef2  26188  rlimcnp  26927  noetalem1  27705  addsproplem2  27929  ex-un  30405  shs0i  31430  chj0i  31436  disjun0  32576  ffsrn  32706  difioo  32759  symgcom2  33095  eulerpartlemt  34403  fineqvac  35128  subfacp1lem1  35201  cvmscld  35295  mthmpps  35604  refssfne  36376  topjoin  36383  pibt2  37435  poimirlem3  37647  poimirlem28  37672  rntrclfvOAI  42714  istopclsd  42723  nacsfix  42735  diophrw  42782  tfsconcatb0  43368  onsucunipr  43396  oaun3  43406  clcnvlem  43647  cnvrcl0  43649  dmtrcl  43651  rntrcl  43652  iunrelexp0  43726  dmtrclfvRP  43754  rntrclfv  43756  cotrclrcl  43766  clsk3nimkb  44064  limciccioolb  45650  limcicciooub  45666  ioccncflimc  45914  icocncflimc  45918  stoweidlem44  46073  dirkercncflem3  46134  fourierdlem62  46197  ismeannd  46496  cycl3grtri  47959