Theorem eldif 2054

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 1814	. 2 |- (A e. (B \ C) -> A e. V)
2		elisset 1814	. . 3 |- (A e. B -> A e. V)
3	2	adantr 389	. 2 |- ((A e. B /\ -. A e. C) -> A e. V)
4		eleq1 1532	. . . 4 |- (x = A -> (x e. B <-> A e. B))
5		eleq1 1532	. . . . 5 |- (x = A -> (x e. C <-> A e. C))
6	5	negbid 610	. . . 4 |- (x = A -> (-. x e. C <-> -. A e. C))
7	4, 6	anbi12d 627	. . 3 |- (x = A -> ((x e. B /\ -. x e. C) <-> (A e. B /\ -. A e. C)))
8		df-dif 2046	. . 3 |- (B \ C) = {x | (x e. B /\ -. x e. C)}
9	7, 8	elab2g 1897	. 2 |- (A e. V -> (A e. (B \ C) <-> (A e. B /\ -. A e. C)))
10	1, 3, 9	pm5.21nii 678	1 |- (A e. (B \ C) <-> (A e. B /\ -. A e. C))

Syntax hints:  -. wn 2   <-> wb 146   /\ wa 223   = wceq 955   e. wcel 957  Vcvv 1808   \ cdif 2041

This theorem is referenced by:  hbdif 2158  eldifi 2159  eldifn 2160  neldif 2162  difdif 2163  ddif 2166  ssconb 2167  sscon 2168  ssdif 2169  dfss4 2239  dfun2 2240  dfin2 2241  difin 2242  symdif2 2263  dfnul2 2279  reldisj 2310  disj3 2311  undif4 2322  ssdif0 2324  pssnel 2328  difin0ss 2329  inssdif0 2330  ssundif 2341  eldifsn 2459  iundif2 2606  iindif2 2607  pwundif 2824  eldifpw 2906  elpwunsn 2908  ordunidif 3001  onmindif 3056  opelxpex2 3275  imadif 3570  oelim2 4215  oaabs 4245  brsdom 4372  brsdom2 4450  php3 4504  unblem1 4526  unfilem1 4533  infeq5 4604  kmlem4 4751  xrlenltt 5484  clsval2 7645  elcls 7664  islp2 7707  metelcls 7927  grothprim 8738  strlem1 10133  strlem5 10138  hstrlem5 10146

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171  df-clab 1463  df-cleq 1468  df-clel 1471  df-v 1809  df-dif 2046

Copyright terms: Public domain