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

Theorem ssequn2 3743
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 3740 . 2 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐵)
2 uncom 3714 . . 3 (𝐴𝐵) = (𝐵𝐴)
32eqeq1i 2610 . 2 ((𝐴𝐵) = 𝐵 ↔ (𝐵𝐴) = 𝐵)
41, 3bitri 262 1 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474  cun 3533  wss 3535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-un 3540  df-in 3542  df-ss 3549
This theorem is referenced by:  unabs  3811  tppreqb  4272  pwssun  4930  pwundif  4931  relresfld  5561  ordssun  5726  ordequn  5727  oneluni  5739  fsnunf  6330  sorpssun  6815  ordunpr  6891  fodomr  7969  enp1ilem  8052  pwfilem  8116  brwdom2  8334  sucprcreg  8362  dfacfin7  9077  hashbclem  13041  incexclem  14349  ramub1lem1  15510  ramub1lem2  15511  mreexmrid  16068  lspun0  18774  lbsextlem4  18924  cldlp  20702  ordtuni  20742  lfinun  21076  cldsubg  21662  trust  21781  nulmbl2  23024  limcmpt2  23367  cnplimc  23370  dvreslem  23392  dvaddbr  23420  dvmulbr  23421  lhop  23496  plypf1  23685  coeeulem  23697  coeeu  23698  coef2  23704  rlimcnp  24405  ex-un  26435  shs0i  27494  chj0i  27500  disjun0  28592  ffsrn  28694  difioo  28736  eulerpartlemt  29562  subfacp1lem1  30217  cvmscld  30311  mthmpps  30535  refssfne  31325  topjoin  31332  poimirlem3  32381  poimirlem28  32406  rntrclfvOAI  36071  istopclsd  36080  nacsfix  36092  diophrw  36139  clcnvlem  36748  cnvrcl0  36750  dmtrcl  36752  rntrcl  36753  iunrelexp0  36812  dmtrclfvRP  36840  rntrclfv  36842  cotrclrcl  36852  clsk3nimkb  37157  limciccioolb  38488  limcicciooub  38504  ioccncflimc  38571  icocncflimc  38575  stoweidlem44  38737  dirkercncflem3  38798  fourierdlem62  38861  ismeannd  39160
  Copyright terms: Public domain W3C validator