Theorem eldif 2047

Description: Expansion of membership in a class difference.

Assertion

Ref	Expression
eldif	|- (A e. (B \ C) <-> (A e. B /\ -. A e. C))

Proof of Theorem eldif

Step	Hyp	Ref	Expression
1		elisset 1808	. 2 |- (A e. (B \ C) -> A e. V)
2		elisset 1808	. . 3 |- (A e. B -> A e. V)
3	2	adantr 389	. 2 |- ((A e. B /\ -. A e. C) -> A e. V)
4		eleq1 1526	. . . 4 |- (x = A -> (x e. B <-> A e. B))
5		eleq1 1526	. . . . 5 |- (x = A -> (x e. C <-> A e. C))
6	5	negbid 609	. . . 4 |- (x = A -> (-. x e. C <-> -. A e. C))
7	4, 6	anbi12d 626	. . 3 |- (x = A -> ((x e. B /\ -. x e. C) <-> (A e. B /\ -. A e. C)))
8		df-dif 2039	. . 3 |- (B \ C) = {x | (x e. B /\ -. x e. C)}
9	7, 8	elab2g 1891	. 2 |- (A e. V -> (A e. (B \ C) <-> (A e. B /\ -. A e. C)))
10	1, 3, 9	pm5.21nii 677	1 |- (A e. (B \ C) <-> (A e. B /\ -. A e. C))

Syntax hints:  -. wn 2   <-> wb 146   /\ wa 223   = wceq 953   e. wcel 955  Vcvv 1802   \ cdif 2034

This theorem is referenced by:  hbdif 2151  eldifi 2152  eldifn 2153  neldif 2155  difdif 2156  ddif 2159  ssconb 2160  sscon 2161  ssdif 2162  dfss4 2232  dfun2 2233  dfin2 2234  difin 2235  symdif2 2256  dfnul2 2272  reldisj 2303  disj3 2304  undif4 2315  ssdif0 2317  pssnel 2321  difin0ss 2322  inssdif0 2323  ssundif 2334  eldifsn 2453  iundif2 2600  iindif2 2601  pwundif 2817  eldifpw 2900  elpwunsn 2902  ordunidif 2995  onmindif 3050  imadif 3560  oelim2 4206  oaabs 4236  brsdom 4363  brsdom2 4441  php3 4495  unblem1 4517  unfilem1 4524  infeq5 4593  kmlem4 4740  xrlenltt 5473  clsval2 7627  elcls 7646  islp2 7688  metelcls 7900  grothprim 8722  strlem1 10087  strlem5 10092  hstrlem5 10100

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-dif 2039

Copyright terms: Public domain