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

Theorem dfss1 3560
Description: A frequently-used variant of subclass definition df-ss 3347. (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 3347 . 2  |-  ( A 
C_  B  <->  ( A  i^i  B )  =  A )
2 incom 3548 . . 3  |-  ( A  i^i  B )  =  ( B  i^i  A
)
32eqeq1i 2450 . 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 1369    i^i cin 3332    C_ wss 3333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-in 3340  df-ss 3347
This theorem is referenced by:  dfss5  3561  sseqin2  3574  onfr  4763  xpimasnOLD  5289  fndmdif  5812  sorpssin  6373  infxpenlem  8185  acndom2  8229  isf34lem5  8552  fpwwe2  8815  leiso  12217  isercolllem3  13149  incexc  13305  bitsinv1  13643  bitsinvp1  13650  bitsshft  13676  ressabs  14241  psssdm  15391  dprdsn  16538  ablfac1eu  16579  ablfaclem3  16593  ocv1  18109  resttopon  18770  restabs  18774  restopnb  18784  restperf  18793  ordtbas  18801  ordtrest2lem  18812  ordtrest2  18813  leordtvallem1  18819  leordtvallem2  18820  cnclsi  18881  ordtt1  18988  connsub  19030  cnconn  19031  nconsubb  19032  consubclo  19033  1stcfb  19054  kgentopon  19116  ptbasfi  19159  ptclsg  19193  dfac14lem  19195  xkoccn  19197  txcnmpt  19202  txtube  19218  xkoptsub  19232  xkopt  19233  kqsat  19309  kqcldsat  19311  ordthmeolem  19379  trfil1  19464  trfil2  19465  trufil  19488  divstgphaus  19698  trust  19809  metustfbasOLD  20145  metustfbas  20146  cfilucfilOLD  20149  cfilucfil  20150  xrsmopn  20394  lebnumii  20543  iscmet3  20809  resscdrg  20875  uniioombllem4  21071  mbflimsup  21149  lhop1  21491  lhop2  21492  wilthlem2  22412  ex-in  23637  fimacnvinrn2  25958  xppreima  25969  gtiso  26001  resf1o  26035  prsss  26351  ordtrestNEW  26356  ordtrest2NEWlem  26357  ordtrest2NEW  26358  probdsb  26810  totprobd  26814  cndprobtot  26824  ballotlemfmpn  26882  signsplypnf  26956  signsply0  26957  omsinds  27685  mblfinlem3  28435  mblfinlem4  28436  itg2addnclem2  28449  neibastop3  28588  sstotbnd2  28678  stoweidlem50  29850  lcvexchlem4  32687  lclkrlem2r  35174  mapdunirnN  35300
  Copyright terms: Public domain W3C validator