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

Theorem dfss1 3386
Description: A frequently-used variant of subclass definition df-ss 3179. (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 3179 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 incom 3374 . . 3  |-  ( A  i^i  B )  =  ( B  i^i  A
)
32eqeq1i 2303 . 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 1632    i^i cin 3164    C_ wss 3165
This theorem is referenced by:  dfss5  3387  sseqin2  3401  onfr  4447  fndmdif  5645  sorpssin  6301  infxpenlem  7657  acndom2  7697  isf34lem5  8020  fpwwe2  8281  leiso  11413  isercolllem3  12156  incexc  12312  bitsinv1  12649  bitsinvp1  12656  bitsshft  12682  ressabs  13222  psssdm  14341  dprdsn  15287  ablfac1eu  15324  ablfaclem3  15338  ocv1  16595  resttopon  16908  restabs  16912  restopnb  16922  restperf  16930  ordtbas  16938  ordtrest2lem  16949  ordtrest2  16950  leordtvallem1  16956  leordtvallem2  16957  cnclsi  17017  ordtt1  17123  connsub  17163  cnconn  17164  nconsubb  17165  consubclo  17166  1stcfb  17187  kgentopon  17249  ptbasfi  17292  ptclsg  17325  dfac14lem  17327  xkoccn  17329  txcnmpt  17334  txtube  17350  xkoptsub  17364  xkopt  17365  kqsat  17438  kqcldsat  17440  ordthmeolem  17508  trfil1  17597  trfil2  17598  trufil  17621  divstgphaus  17821  xrsmopn  18334  lebnumii  18480  iscmet3  18735  resscdrg  18791  uniioombllem4  18957  mbflimsup  19037  lhop1  19377  lhop2  19378  wilthlem2  20323  ex-in  20828  fimacnvinrn2  23215  xppreima  23226  gtiso  23256  probdsb  23640  cndprobtot  23654  omsinds  24290  itg2addnclem2  25004  islimrs3  25684  neibastop3  26414  sstotbnd2  26601  stoweidlem50  27902  lcvexchlem4  29849  lclkrlem2r  32336  mapdunirnN  32462
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-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator