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

Theorem ssequn2 3348
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 3345 . 2  |-  ( A 
C_  B  <->  ( A  u.  B )  =  B )
2 uncom 3319 . . 3  |-  ( A  u.  B )  =  ( B  u.  A
)
32eqeq1i 2290 . 2  |-  ( ( A  u.  B )  =  B  <->  ( B  u.  A )  =  B )
41, 3bitri 240 1  |-  ( A 
C_  B  <->  ( B  u.  A )  =  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623    u. cun 3150    C_ wss 3152
This theorem is referenced by:  unabs  3399  pwssun  4299  pwundif  4300  ordssun  4492  ordequn  4493  oneluni  4505  ordunpr  4617  relresfld  5199  relcoi1  5201  fsnunf  5718  sorpssun  6284  fodomr  7012  enp1ilem  7092  pwfilem  7150  brwdom2  7287  dfacfin7  8025  hashbclem  11390  incexclem  12295  ramub1lem1  13073  ramub1lem2  13074  mreexmrid  13545  lspun0  15768  lbsextlem4  15914  cldlp  16881  ordtuni  16920  cldsubg  17793  nulmbl2  18894  limcmpt2  19234  cnplimc  19237  dvreslem  19259  dvaddbr  19287  dvmulbr  19288  lhop  19363  plypf1  19594  coeeulem  19606  coeeu  19607  coef2  19613  rlimcnp  20260  ex-un  20811  shs0i  22028  chj0i  22034  pwundif2  23186  difioo  23275  subfacp1lem1  23710  cvmscld  23804  refssfne  26294  topjoin  26314  istopclsd  26775  nacsfix  26787  diophrw  26838  stoweidlem44  27793
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-un 3157  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator