Theorem dfss 2051

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

Assertion

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

Proof of Theorem dfss

Step	Hyp	Ref	Expression
1		df-ss 2050	. 2 |- (A (_ B <-> (A i^i B) = A)
2		eqcom 1475	. 2 |- ((A i^i B) = A <-> A = (A i^i B))
3	1, 2	bitr 173	1 |- (A (_ B <-> A = (A i^i B))

Syntax hints:   <-> wb 146   = wceq 955   i^i cin 2043   (_ wss 2044

This theorem is referenced by:  dfss2 2055  wefrc 2939  onelin 3099  cnvcnv 3482  funimass1 3568  tz7.44-2 3924  tz7.44-3 3925  frfnom 3946  sbthlem5 4440  abfii2 4545  dmaddpi 5001  dmmulpi 5002  metssba2 7770  mdbr3 10180  mdbr4 10181  ssmd1 10194  stoi 10555

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-4 972  ax-5o 974  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1468  df-ss 2050

Copyright terms: Public domain