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

Theorem dfss1 3373
Description: A frequently-used variant of subclass definition df-ss 3166. (Contributed by NM, 10-Jan-2015.)
Assertion
Ref Expression
dfss1  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )

Proof of Theorem dfss1
StepHypRef Expression
1 df-ss 3166 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 incom 3361 . . 3  |-  ( A  i^i  B )  =  ( B  i^i  A
)
32eqeq1i 2290 . 2  |-  ( ( A  i^i  B )  =  A  <->  ( B  i^i  A )  =  A )
41, 3bitri 240 1  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623    i^i cin 3151    C_ wss 3152
This theorem is referenced by:  dfss5  3374  sseqin2  3388  onfr  4431  fndmdif  5629  sorpssin  6285  infxpenlem  7641  acndom2  7681  isf34lem5  8004  fpwwe2  8265  leiso  11397  isercolllem3  12140  incexc  12296  bitsinv1  12633  bitsinvp1  12640  bitsshft  12666  ressabs  13206  psssdm  14325  dprdsn  15271  ablfac1eu  15308  ablfaclem3  15322  ocv1  16579  resttopon  16892  restabs  16896  restopnb  16906  restperf  16914  ordtbas  16922  ordtrest2lem  16933  ordtrest2  16934  leordtvallem1  16940  leordtvallem2  16941  cnclsi  17001  ordtt1  17107  connsub  17147  cnconn  17148  nconsubb  17149  consubclo  17150  1stcfb  17171  kgentopon  17233  ptbasfi  17276  ptclsg  17309  dfac14lem  17311  xkoccn  17313  txcnmpt  17318  txtube  17334  xkoptsub  17348  xkopt  17349  kqsat  17422  kqcldsat  17424  ordthmeolem  17492  trfil1  17581  trfil2  17582  trufil  17605  divstgphaus  17805  xrsmopn  18318  lebnumii  18464  iscmet3  18719  resscdrg  18775  uniioombllem4  18941  mbflimsup  19021  lhop1  19361  lhop2  19362  wilthlem2  20307  ex-in  20812  fimacnvinrn2  23200  xppreima  23211  gtiso  23241  probdsb  23625  cndprobtot  23639  omsinds  24219  islimrs3  25581  neibastop3  26311  sstotbnd2  26498  stoweidlem50  27799  lcvexchlem4  29227  lclkrlem2r  31714  mapdunirnN  31840
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-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator