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

Theorem dfss1 3644
Description: A frequently-used variant of subclass definition df-ss 3428. (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 3428 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 incom 3632 . . 3  |-  ( A  i^i  B )  =  ( B  i^i  A
)
32eqeq1i 2409 . 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 1405    i^i cin 3413    C_ wss 3414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-v 3061  df-in 3421  df-ss 3428
This theorem is referenced by:  dfss5  3645  sseqin2  3658  onfr  5449  fndmdif  5969  fveqressseq  6005  sorpssin  6570  omsinds  6702  infxpenlem  8423  acndom2  8467  isf34lem5  8790  fpwwe2  9051  leiso  12557  isercolllem3  13638  incexc  13800  bitsinv1  14301  bitsinvp1  14308  bitsshft  14334  ressabs  14907  psssdm  16170  dprdsn  17403  ablfac1eu  17444  ablfaclem3  17458  ocv1  19008  resttopon  19955  restabs  19959  restopnb  19969  restperf  19978  ordtbas  19986  ordtrest2lem  19997  ordtrest2  19998  leordtvallem1  20004  leordtvallem2  20005  cnclsi  20066  ordtt1  20173  connsub  20214  cnconn  20215  nconsubb  20216  consubclo  20217  1stcfb  20238  kgentopon  20331  ptbasfi  20374  ptclsg  20408  dfac14lem  20410  xkoccn  20412  txcnmpt  20417  txtube  20433  xkoptsub  20447  xkopt  20448  kqsat  20524  kqcldsat  20526  ordthmeolem  20594  trfil1  20679  trfil2  20680  trufil  20703  qustgphaus  20913  trust  21024  metustfbasOLD  21360  metustfbas  21361  cfilucfilOLD  21364  cfilucfil  21365  xrsmopn  21609  lebnumii  21758  iscmet3  22024  resscdrg  22090  uniioombllem4  22287  mbflimsup  22365  lhop1  22707  lhop2  22708  wilthlem2  23724  ex-in  25563  fimacnvinrn2  27919  xppreima  27930  gtiso  27963  resf1o  28000  prsss  28351  ordtrestNEW  28356  ordtrest2NEWlem  28357  ordtrest2NEW  28358  carsggect  28766  probdsb  28867  totprobd  28871  cndprobtot  28881  ballotlemfmpn  28939  signsplypnf  29013  signsply0  29014  neibastop3  30590  topdifinfeq  31267  mblfinlem3  31425  mblfinlem4  31426  itg2addnclem2  31440  sstotbnd2  31552  lcvexchlem4  32055  lclkrlem2r  34544  mapdunirnN  34670  wnefimgd  35985  stoweidlem50  37200
  Copyright terms: Public domain W3C validator