Theorem dfss 2869

Description: A frequently-used variant of subclass definition df-ss 2868.

Assertion

Ref	Expression
dfss	|- (A C_ B <-> A = (A i^i B))

Proof of Theorem dfss

Step	Hyp	Ref	Expression
1		df-ss 2868	. 2 |- (A C_ B <-> (A i^i B) = A)
2		eqcom 2172	. 2 |- ((A i^i B) = A <-> A = (A i^i B))
3	1, 2	bitri 306	1 |- (A C_ B <-> A = (A i^i B))

Syntax hints:   <-> wb 231   = wceq 1615   i^i cin 2858   C_ wss 2859

This theorem is referenced by:  dfss2 2873  iinrab2 3521  wefrc 3838  onelini 3953  cnvcnv 4503  funimass1 4629  tz7.44-2 5341  tz7.44-3 5342  frfnom 5363  sbthlem5 5723  abfii2 5918  dmaddpi 6613  dmmulpi 6614  metssba2 10103  stoiglemOLD 11244  stoiglem 11245  mdbr3 12858  mdbr4 12859  ssmd1 12872  stoi 16050  stoiOLD 16051  compsublem 16515  subspopn 16922  subspcld 16923  bndss 17027

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1622  ax-4 1637  ax-5o 1639  ax-ext 2152

This theorem depends on definitions:  df-bi 232  df-cleq 2163  df-ss 2868

Copyright terms: Public domain