Theorem eldif 2144

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 1895	. 2 |- (A e. (B \ C) -> A e. V)
2		elisset 1895	. . 3 |- (A e. B -> A e. V)
3	2	adantr 399	. 2 |- ((A e. B /\ -. A e. C) -> A e. V)
4		eleq1 1605	. . . 4 |- (x = A -> (x e. B <-> A e. B))
5		eleq1 1605	. . . . 5 |- (x = A -> (x e. C <-> A e. C))
6	5	notbid 634	. . . 4 |- (x = A -> (-. x e. C <-> -. A e. C))
7	4, 6	anbi12d 651	. . 3 |- (x = A -> ((x e. B /\ -. x e. C) <-> (A e. B /\ -. A e. C)))
8		df-dif 2134	. . 3 |- (B \ C) = {x | (x e. B /\ -. x e. C)}
9	7, 8	elab2g 1978	. 2 |- (A e. V -> (A e. (B \ C) <-> (A e. B /\ -. A e. C)))
10	1, 3, 9	pm5.21nii 703	1 |- (A e. (B \ C) <-> (A e. B /\ -. A e. C))

Syntax hints:  -. wn 2   <-> wb 152   /\ wa 229   = wceq 1018   e. wcel 1020  Vcvv 1888   \ cdif 2128

This theorem is referenced by:  hbdif 2248  eldifi 2249  eldifn 2250  neldif 2252  difdif 2253  ddif 2256  ssconb 2257  sscon 2258  ssdif 2259  dfss4 2329  dfun2 2330  dfin2 2331  difin 2332  symdif2 2353  dfnul2 2369  reldisj 2401  disj3 2402  undif4 2413  ssdif0 2415  pssnel 2419  difin0ss 2420  inssdif0 2421  ssundif 2433  eldifsn 2565  iundif2 2719  iindif2 2721  pwundif 2946  ordunidif 3062  onmindif 3101  eldifpw 3173  elpwunsn 3175  opelxpex2 3409  dfco2a 3640  imadif 3721  dffv2 3926  oelim2 4401  oaabs 4435  brsdom 4565  brsdom2 4649  php3 4705  unblem1 4729  unfilem1 4737  infeq5 4809  kmlem4 4957  xrlenlt 5698  irradd 6459  irrmul 6460  modirr 6524  clsval2 7945  elcls 7964  islp2 8007  metelcls 8226  grothprim 9123  strlem1 10524  strlem5 10529  hstrlem5 10537  mlteqer 10854  cdrci 11133  subntr 11618  cptclsscpt 11625  hscptsscld 11627  alexsublem3 11634  locfincomp 11711  ist1-2 11739  fixufil 11797  ufinffr 11799  difin2 11909  difxp 11913  fimax 11947  recms 12163

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1024  ax-gen 1025  ax-8 1026  ax-10 1028  ax-12 1030  ax-17 1033  ax-4 1035  ax-5o 1037  ax-6o 1040  ax-9o 1185  ax-10o 1203  ax-16 1273  ax-11o 1281  ax-ext 1528

This theorem depends on definitions:  df-bi 153  df-an 231  df-ex 1043  df-sb 1235  df-clab 1534  df-cleq 1539  df-clel 1542  df-v 1890  df-dif 2134

Copyright terms: Public domain