Theorem dfss4 3858

Description: Subclass defined in terms of class difference. See comments under dfun2 3859. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

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

Proof of Theorem dfss4

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sseqin2 3817	. 2 |- ( A C_ B <-> ( B i^i A ) = A )
2		eldif 3584	. . . . . . 7 |- ( x e. ( B \ A ) <-> ( x e. B /\ -. x e. A ) )
3	2	notbii 310	. . . . . 6 |- ( -. x e. ( B \ A ) <-> -. ( x e. B /\ -. x e. A ) )
4	3	anbi2i 730	. . . . 5 |- ( ( x e. B /\ -. x e. ( B \ A ) ) <-> ( x e. B /\ -. ( x e. B /\ -. x e. A ) ) )
5		elin 3796	. . . . . 6 |- ( x e. ( B i^i A ) <-> ( x e. B /\ x e. A ) )
6		abai 836	. . . . . 6 |- ( ( x e. B /\ x e. A ) <-> ( x e. B /\ ( x e. B -> x e. A ) ) )
7		iman 440	. . . . . . 7 |- ( ( x e. B -> x e. A ) <-> -. ( x e. B /\ -. x e. A ) )
8	7	anbi2i 730	. . . . . 6 |- ( ( x e. B /\ ( x e. B -> x e. A ) ) <-> ( x e. B /\ -. ( x e. B /\ -. x e. A ) ) )
9	5, 6, 8	3bitri 286	. . . . 5 |- ( x e. ( B i^i A ) <-> ( x e. B /\ -. ( x e. B /\ -. x e. A ) ) )
10	4, 9	bitr4i 267	. . . 4 |- ( ( x e. B /\ -. x e. ( B \ A ) ) <-> x e. ( B i^i A ) )
11	10	difeqri 3730	. . 3 |- ( B \ ( B \ A ) ) = ( B i^i A )
12	11	eqeq1i 2627	. 2 |- ( ( B \ ( B \ A ) ) = A <-> ( B i^i A ) = A )
13	1, 12	bitr4i 267	1 |- ( A C_ B <-> ( B \ ( B \ A ) ) = A )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   \ cdif 3571   i^i cin 3573   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588

This theorem is referenced by:  ssdifim  3862  dfin4  3867  sorpsscmpl  6948  sbthlem3  8072  fin23lem7  9138  fin23lem11  9139  compsscnvlem  9192  compssiso  9196  isf34lem4  9199  efgmnvl  18127  frlmlbs  20136  isopn2  20836  iincld  20843  iuncld  20849  clsval2  20854  ntrval2  20855  ntrdif  20856  clsdif  20857  cmclsopn  20866  opncldf1  20888  indiscld  20895  mretopd  20896  restcld  20976  pnrmopn  21147  conndisj  21219  hausllycmp  21297  kqcldsat  21536  filufint  21724  cfinufil  21732  ufilen  21734  alexsublem  21848  bcth3  23128  inmbl  23310  iccmbl  23334  mbfimaicc  23400  i1fd  23448  itgss3  23581  difuncomp  29369  iundifdifd  29380  iundifdif  29381  cldssbrsiga  30250  unelcarsg  30374  kur14lem4  31191  cldbnd  32321  clsun  32323  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  itg2addnclem  33461  fdc  33541  dssmapnvod  38314  sscon34b  38317  ntrclsfveq1  38358  ntrclsfveq  38360  ntrclsneine0lem  38362  ntrclsiso  38365  ntrclsk2  38366  ntrclskb  38367  ntrclsk3  38368  ntrclsk13  38369  ntrclsk4  38370  clsneiel2  38407  neicvgel2  38418  salincl  40543  salexct  40552  ovnsubadd2lem  40859  lincext2  42244