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

Theorem ssequn2 3361
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 3358 . 2  |-  ( A 
C_  B  <->  ( A  u.  B )  =  B )
2 uncom 3332 . . 3  |-  ( A  u.  B )  =  ( B  u.  A
)
32eqeq1i 2303 . 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 1632    u. cun 3163    C_ wss 3165
This theorem is referenced by:  unabs  3412  pwssun  4315  pwundif  4316  ordssun  4508  ordequn  4509  oneluni  4521  ordunpr  4633  relresfld  5215  relcoi1  5217  fsnunf  5734  sorpssun  6300  fodomr  7028  enp1ilem  7108  pwfilem  7166  brwdom2  7303  dfacfin7  8041  hashbclem  11406  incexclem  12311  ramub1lem1  13089  ramub1lem2  13090  mreexmrid  13561  lspun0  15784  lbsextlem4  15930  cldlp  16897  ordtuni  16936  cldsubg  17809  nulmbl2  18910  limcmpt2  19250  cnplimc  19253  dvreslem  19275  dvaddbr  19303  dvmulbr  19304  lhop  19379  plypf1  19610  coeeulem  19622  coeeu  19623  coef2  19629  rlimcnp  20276  ex-un  20827  shs0i  22044  chj0i  22050  pwundif2  23202  difioo  23290  subfacp1lem1  23725  cvmscld  23819  refssfne  26397  topjoin  26417  istopclsd  26878  nacsfix  26890  diophrw  26941  stoweidlem44  27896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator