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

Theorem ssequn2 4162
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 4159 . 2 (𝐴𝐵 ↔ (𝐴𝐵) = 𝐵)
2 uncom 4132 . . 3 (𝐴𝐵) = (𝐵𝐴)
32eqeq1i 2830 . 2 ((𝐴𝐵) = 𝐵 ↔ (𝐵𝐴) = 𝐵)
41, 3bitri 276 1 (𝐴𝐵 ↔ (𝐵𝐴) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1530  cun 3937  wss 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-v 3501  df-un 3944  df-in 3946  df-ss 3955
This theorem is referenced by:  unabs  4234  tppreqb  4736  pwssun  5453  pwundifOLD  5455  relresfld  6124  ordssun  6287  ordequn  6288  oneluni  6300  fsnunf  6946  sorpssun  7449  ordunpr  7532  fodomr  8660  enp1ilem  8744  pwfilem  8810  brwdom2  9029  sucprcreg  9057  dfacfin7  9813  hashbclem  13803  incexclem  15183  ramub1lem1  16354  ramub1lem2  16355  mreexmrid  16906  lspun0  19705  lbsextlem4  19855  cldlp  21676  ordtuni  21716  lfinun  22051  cldsubg  22636  trust  22755  nulmbl2  24054  limcmpt2  24399  cnplimc  24402  dvreslem  24424  dvaddbr  24452  dvmulbr  24453  lhop  24530  plypf1  24719  coeeulem  24731  coeeu  24732  coef2  24738  rlimcnp  25459  ex-un  28119  shs0i  29142  chj0i  29148  disjun0  30262  ffsrn  30380  difioo  30420  symgcom2  30644  eulerpartlemt  31517  subfacp1lem1  32312  cvmscld  32406  mthmpps  32715  refssfne  33592  topjoin  33599  pibt2  34569  poimirlem3  34764  poimirlem28  34789  rntrclfvOAI  39155  istopclsd  39164  nacsfix  39176  diophrw  39223  clcnvlem  39850  cnvrcl0  39852  dmtrcl  39854  rntrcl  39855  iunrelexp0  39914  dmtrclfvRP  39942  rntrclfv  39944  cotrclrcl  39954  clsk3nimkb  40257  limciccioolb  41769  limcicciooub  41785  ioccncflimc  42035  icocncflimc  42039  stoweidlem44  42197  dirkercncflem3  42258  fourierdlem62  42321  ismeannd  42617
  Copyright terms: Public domain W3C validator