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

Theorem dfss1 3703
Description: A frequently-used variant of subclass definition df-ss 3490. (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 3490 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 incom 3691 . . 3  |-  ( A  i^i  B )  =  ( B  i^i  A
)
32eqeq1i 2474 . 2  |-  ( ( A  i^i  B )  =  A  <->  ( B  i^i  A )  =  A )
41, 3bitri 249 1  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1379    i^i cin 3475    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483  df-ss 3490
This theorem is referenced by:  dfss5  3704  sseqin2  3717  onfr  4917  xpimasnOLD  5451  fndmdif  5983  sorpssin  6570  infxpenlem  8387  acndom2  8431  isf34lem5  8754  fpwwe2  9017  leiso  12470  isercolllem3  13448  incexc  13608  bitsinv1  13947  bitsinvp1  13954  bitsshft  13980  ressabs  14549  psssdm  15699  dprdsn  16873  ablfac1eu  16914  ablfaclem3  16928  ocv1  18477  resttopon  19428  restabs  19432  restopnb  19442  restperf  19451  ordtbas  19459  ordtrest2lem  19470  ordtrest2  19471  leordtvallem1  19477  leordtvallem2  19478  cnclsi  19539  ordtt1  19646  connsub  19688  cnconn  19689  nconsubb  19690  consubclo  19691  1stcfb  19712  kgentopon  19774  ptbasfi  19817  ptclsg  19851  dfac14lem  19853  xkoccn  19855  txcnmpt  19860  txtube  19876  xkoptsub  19890  xkopt  19891  kqsat  19967  kqcldsat  19969  ordthmeolem  20037  trfil1  20122  trfil2  20123  trufil  20146  divstgphaus  20356  trust  20467  metustfbasOLD  20803  metustfbas  20804  cfilucfilOLD  20807  cfilucfil  20808  xrsmopn  21052  lebnumii  21201  iscmet3  21467  resscdrg  21533  uniioombllem4  21730  mbflimsup  21808  lhop1  22150  lhop2  22151  wilthlem2  23071  ex-in  24823  fimacnvinrn2  27149  xppreima  27159  gtiso  27191  resf1o  27225  prsss  27534  ordtrestNEW  27539  ordtrest2NEWlem  27540  ordtrest2NEW  27541  probdsb  28001  totprobd  28005  cndprobtot  28015  ballotlemfmpn  28073  signsplypnf  28147  signsply0  28148  omsinds  28876  mblfinlem3  29630  mblfinlem4  29631  itg2addnclem2  29644  neibastop3  29783  sstotbnd2  29873  stoweidlem50  31350  lcvexchlem4  33834  lclkrlem2r  36321  mapdunirnN  36447
  Copyright terms: Public domain W3C validator