MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssequn2 Structured version   Visualization version   GIF version

Theorem ssequn2 3748
Description: A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.)
Assertion
Ref Expression
ssequn2 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐵)

Proof of Theorem ssequn2
StepHypRef Expression
1 ssequn1 3745 . 2 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐵)
2 uncom 3719 . . 3 (𝐴𝐵) = (𝐵𝐴)
32eqeq1i 2615 . 2 ((𝐴𝐵) = 𝐵 ↔ (𝐵𝐴) = 𝐵)
41, 3bitri 263 1 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 195   = wceq 1475  cun 3538  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554
This theorem is referenced by:  unabs  3816  tppreqb  4277  pwssun  4944  pwundif  4945  relresfld  5579  ordssun  5744  ordequn  5745  oneluni  5757  fsnunf  6356  sorpssun  6842  ordunpr  6918  fodomr  7996  enp1ilem  8079  pwfilem  8143  brwdom2  8361  sucprcreg  8389  dfacfin7  9104  hashbclem  13093  incexclem  14407  ramub1lem1  15568  ramub1lem2  15569  mreexmrid  16126  lspun0  18832  lbsextlem4  18982  cldlp  20764  ordtuni  20804  lfinun  21138  cldsubg  21724  trust  21843  nulmbl2  23111  limcmpt2  23454  cnplimc  23457  dvreslem  23479  dvaddbr  23507  dvmulbr  23508  lhop  23583  plypf1  23772  coeeulem  23784  coeeu  23785  coef2  23791  rlimcnp  24492  ex-un  26673  shs0i  27692  chj0i  27698  disjun0  28790  ffsrn  28892  difioo  28934  eulerpartlemt  29760  subfacp1lem1  30415  cvmscld  30509  mthmpps  30733  refssfne  31523  topjoin  31530  poimirlem3  32582  poimirlem28  32607  rntrclfvOAI  36272  istopclsd  36281  nacsfix  36293  diophrw  36340  clcnvlem  36949  cnvrcl0  36951  dmtrcl  36953  rntrcl  36954  iunrelexp0  37013  dmtrclfvRP  37041  rntrclfv  37043  cotrclrcl  37053  clsk3nimkb  37358  limciccioolb  38688  limcicciooub  38704  ioccncflimc  38771  icocncflimc  38775  stoweidlem44  38937  dirkercncflem3  38998  fourierdlem62  39061  ismeannd  39360
  Copyright terms: Public domain W3C validator