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

Theorem dfss1 3505
Description: A frequently-used variant of subclass definition df-ss 3294. (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 3294 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 incom 3493 . . 3  |-  ( A  i^i  B )  =  ( B  i^i  A
)
32eqeq1i 2411 . 2  |-  ( ( A  i^i  B )  =  A  <->  ( B  i^i  A )  =  A )
41, 3bitri 241 1  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1649    i^i cin 3279    C_ wss 3280
This theorem is referenced by:  dfss5  3506  sseqin2  3520  onfr  4580  xpimasn  5275  fndmdif  5793  sorpssin  6489  infxpenlem  7851  acndom2  7891  isf34lem5  8214  fpwwe2  8474  leiso  11663  isercolllem3  12415  incexc  12572  bitsinv1  12909  bitsinvp1  12916  bitsshft  12942  ressabs  13482  psssdm  14603  dprdsn  15549  ablfac1eu  15586  ablfaclem3  15600  ocv1  16861  resttopon  17179  restabs  17183  restopnb  17193  restperf  17202  ordtbas  17210  ordtrest2lem  17221  ordtrest2  17222  leordtvallem1  17228  leordtvallem2  17229  cnclsi  17290  ordtt1  17397  connsub  17437  cnconn  17438  nconsubb  17439  consubclo  17440  1stcfb  17461  kgentopon  17523  ptbasfi  17566  ptclsg  17600  dfac14lem  17602  xkoccn  17604  txcnmpt  17609  txtube  17625  xkoptsub  17639  xkopt  17640  kqsat  17716  kqcldsat  17718  ordthmeolem  17786  trfil1  17871  trfil2  17872  trufil  17895  divstgphaus  18105  trust  18212  metustfbasOLD  18548  metustfbas  18549  cfilucfilOLD  18552  cfilucfil  18553  xrsmopn  18796  lebnumii  18944  iscmet3  19199  resscdrg  19265  uniioombllem4  19431  mbflimsup  19511  lhop1  19851  lhop2  19852  wilthlem2  20805  ex-in  21686  fimacnvinrn2  24001  xppreima  24012  gtiso  24041  probdsb  24633  totprobd  24637  cndprobtot  24647  ballotlemfmpn  24705  omsinds  25433  mblfinlem2  26144  mblfinlem3  26145  itg2addnclem2  26156  neibastop3  26281  sstotbnd2  26373  stoweidlem50  27666  lcvexchlem4  29520  lclkrlem2r  32007  mapdunirnN  32133
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator