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

Theorem dfss1 3545
Description: A frequently-used variant of subclass definition df-ss 3334. (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 3334 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 incom 3533 . . 3  |-  ( A  i^i  B )  =  ( B  i^i  A
)
32eqeq1i 2443 . 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 1652    i^i cin 3319    C_ wss 3320
This theorem is referenced by:  dfss5  3546  sseqin2  3560  onfr  4620  xpimasn  5316  fndmdif  5834  sorpssin  6530  infxpenlem  7895  acndom2  7935  isf34lem5  8258  fpwwe2  8518  leiso  11708  isercolllem3  12460  incexc  12617  bitsinv1  12954  bitsinvp1  12961  bitsshft  12987  ressabs  13527  psssdm  14648  dprdsn  15594  ablfac1eu  15631  ablfaclem3  15645  ocv1  16906  resttopon  17225  restabs  17229  restopnb  17239  restperf  17248  ordtbas  17256  ordtrest2lem  17267  ordtrest2  17268  leordtvallem1  17274  leordtvallem2  17275  cnclsi  17336  ordtt1  17443  connsub  17484  cnconn  17485  nconsubb  17486  consubclo  17487  1stcfb  17508  kgentopon  17570  ptbasfi  17613  ptclsg  17647  dfac14lem  17649  xkoccn  17651  txcnmpt  17656  txtube  17672  xkoptsub  17686  xkopt  17687  kqsat  17763  kqcldsat  17765  ordthmeolem  17833  trfil1  17918  trfil2  17919  trufil  17942  divstgphaus  18152  trust  18259  metustfbasOLD  18595  metustfbas  18596  cfilucfilOLD  18599  cfilucfil  18600  xrsmopn  18843  lebnumii  18991  iscmet3  19246  resscdrg  19312  uniioombllem4  19478  mbflimsup  19558  lhop1  19898  lhop2  19899  wilthlem2  20852  ex-in  21733  fimacnvinrn2  24048  xppreima  24059  gtiso  24088  probdsb  24680  totprobd  24684  cndprobtot  24694  ballotlemfmpn  24752  omsinds  25494  mblfinlem3  26245  mblfinlem4  26246  itg2addnclem2  26257  neibastop3  26391  sstotbnd2  26483  stoweidlem50  27775  lcvexchlem4  29835  lclkrlem2r  32322  mapdunirnN  32448
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator