Theorem dfss4 3070

Description: Subclass defined in terms of class difference. See comments under dfun2 3071. (The proof was shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
dfss4	|- (A C_ B <-> (B \ (B \ A)) = A)

Proof of Theorem dfss4

Step	Hyp	Ref	Expression
1		sseqin2 3057	. 2 |- (A C_ B <-> (B i^i A) = A)
2		eldif 2872	. . . . . . 7 |- (x e. (B \ A) <-> (x e. B /\ -. x e. A))
3	2	notbii 362	. . . . . 6 |- (-. x e. (B \ A) <-> -. (x e. B /\ -. x e. A))
4	3	anbi2i 804	. . . . 5 |- ((x e. B /\ -. x e. (B \ A)) <-> (x e. B /\ -. (x e. B /\ -. x e. A)))
5		elin 3031	. . . . . 6 |- (x e. (B i^i A) <-> (x e. B /\ x e. A))
6		abai 898	. . . . . 6 |- ((x e. B /\ x e. A) <-> (x e. B /\ (x e. B -> x e. A)))
7		iman 459	. . . . . . 7 |- ((x e. B -> x e. A) <-> -. (x e. B /\ -. x e. A))
8	7	anbi2i 804	. . . . . 6 |- ((x e. B /\ (x e. B -> x e. A)) <-> (x e. B /\ -. (x e. B /\ -. x e. A)))
9	5, 6, 8	3bitri 334	. . . . 5 |- (x e. (B i^i A) <-> (x e. B /\ -. (x e. B /\ -. x e. A)))
10	4, 9	bitr4i 310	. . . 4 |- ((x e. B /\ -. x e. (B \ A)) <-> x e. (B i^i A))
11	10	difeqri 2979	. . 3 |- (B \ (B \ A)) = (B i^i A)
12	11	eqeq1i 2177	. 2 |- ((B \ (B \ A)) = A <-> (B i^i A) = A)
13	1, 12	bitr4i 310	1 |- (A C_ B <-> (B \ (B \ A)) = A)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 231   /\ wa 433   = wceq 1615   e. wcel 1617   \ cdif 2856   i^i cin 2858   C_ wss 2859

This theorem is referenced by:  dfin4 3076  sbthlem3 5721  isopn2 9960  iincld 9968  ntrval2 9976  cmclsopn 9983  cmntrcld 9984  islp2 10039  subcld 11250  rcfpfillem6 15960  opncldf1 16487  opncldf3 16489  ntrcmp 16491  clscmp 16492  cldbnd 16495  clsun 16498  ufileu 16658  filufint 16659  ufilen 16664  filcon 16665  fcluscf 16697  flimfnfcls 16700  fdc 16897

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-ex 1645  df-sb 1845  df-clab 2158  df-cleq 2163  df-clel 2166  df-v 2571  df-dif 2862  df-in 2866  df-ss 2868

Copyright terms: Public domain