Theorem eldif 2060

Description: Expansion of membership in a class difference.

Assertion

Ref	Expression
eldif	⊢ (A ∈ (B ∖ C) ↔ (A ∈ B ⋀ ¬ A ∈ C))

Proof of Theorem eldif

Step	Hyp	Ref	Expression
1		elisset 1820	. 2 ⊢ (A ∈ (B ∖ C) → A ∈ V)
2		elisset 1820	. . 3 ⊢ (A ∈ B → A ∈ V)
3	2	adantr 391	. 2 ⊢ ((A ∈ B ⋀ ¬ A ∈ C) → A ∈ V)
4		eleq1 1537	. . . 4 ⊢ (x = A → (x ∈ B ↔ A ∈ B))
5		eleq1 1537	. . . . 5 ⊢ (x = A → (x ∈ C ↔ A ∈ C))
6	5	negbid 613	. . . 4 ⊢ (x = A → (¬ x ∈ C ↔ ¬ A ∈ C))
7	4, 6	anbi12d 630	. . 3 ⊢ (x = A → ((x ∈ B ⋀ ¬ x ∈ C) ↔ (A ∈ B ⋀ ¬ A ∈ C)))
8		df-dif 2052	. . 3 ⊢ (B ∖ C) = {x∣(x ∈ B ⋀ ¬ x ∈ C)}
9	7, 8	elab2g 1903	. 2 ⊢ (A ∈ V → (A ∈ (B ∖ C) ↔ (A ∈ B ⋀ ¬ A ∈ C)))
10	1, 3, 9	pm5.21nii 681	1 ⊢ (A ∈ (B ∖ C) ↔ (A ∈ B ⋀ ¬ A ∈ C))

Syntax hints:  ¬ wn 2   ↔ wb 146   ⋀ wa 223   = wceq 958   ∈ wcel 960  Vcvv 1814   ∖ cdif 2047

This theorem is referenced by:  hbdif 2164  eldifi 2165  eldifn 2166  neldif 2168  difdif 2169  ddif 2172  ssconb 2173  sscon 2174  ssdif 2175  dfss4 2245  dfun2 2246  dfin2 2247  difin 2248  symdif2 2269  dfnul2 2285  reldisj 2317  disj3 2318  undif4 2329  ssdif0 2331  pssnel 2335  difin0ss 2336  inssdif0 2337  ssundif 2348  eldifsn 2466  iundif2 2615  iindif2 2616  pwundif 2834  eldifpw 2916  elpwunsn 2918  ordunidif 3011  onmindif 3066  opelxpex2 3285  imadif 3580  oelim2 4228  oaabs 4258  brsdom 4387  brsdom2 4467  php3 4521  php3OLD 4522  unblem1 4551  unfilem1 4560  infeq5 4630  kmlem4 4778  xrlenltt 5513  clsval2 7682  elcls 7701  islp2 7744  metelcls 7962  grothprim 8778  strlem1 10172  strlem5 10177  hstrlem5 10185

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-dif 2052

Copyright terms: Public domain