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

Theorem ssequn2 3464
Description: A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.)
Assertion
Ref Expression
ssequn2  |-  ( A 
C_  B  <->  ( B  u.  A )  =  B )

Proof of Theorem ssequn2
StepHypRef Expression
1 ssequn1 3461 . 2  |-  ( A 
C_  B  <->  ( A  u.  B )  =  B )
2 uncom 3435 . . 3  |-  ( A  u.  B )  =  ( B  u.  A
)
32eqeq1i 2395 . 2  |-  ( ( A  u.  B )  =  B  <->  ( B  u.  A )  =  B )
41, 3bitri 241 1  |-  ( A 
C_  B  <->  ( B  u.  A )  =  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1649    u. cun 3262    C_ wss 3264
This theorem is referenced by:  unabs  3515  tppreqb  3883  pwssun  4431  pwundif  4432  ordssun  4622  ordequn  4623  oneluni  4635  ordunpr  4747  relresfld  5337  relcoi1  5339  fsnunf  5871  sorpssun  6466  fodomr  7195  enp1ilem  7279  pwfilem  7337  brwdom2  7475  dfacfin7  8213  hashbclem  11629  incexclem  12544  ramub1lem1  13322  ramub1lem2  13323  mreexmrid  13796  lspun0  16015  lbsextlem4  16161  cldlp  17137  ordtuni  17177  cldsubg  18062  trust  18181  nulmbl2  19299  limcmpt2  19639  cnplimc  19642  dvreslem  19664  dvaddbr  19692  dvmulbr  19693  lhop  19768  plypf1  19999  coeeulem  20011  coeeu  20012  coef2  20018  rlimcnp  20672  ex-un  21581  shs0i  22800  chj0i  22806  difioo  23982  subfacp1lem1  24645  cvmscld  24740  refssfne  26066  topjoin  26086  istopclsd  26446  nacsfix  26458  diophrw  26509  stoweidlem44  27462
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-v 2902  df-un 3269  df-in 3271  df-ss 3278
  Copyright terms: Public domain W3C validator