Theorem eldif 2609

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 2299	. 2 |- (A e. (B \ C) -> A e. _V)
2		elisset 2299	. . 3 |- (A e. B -> A e. _V)
3	2	adantr 425	. 2 |- ((A e. B /\ -. A e. C) -> A e. _V)
4		eleq1 1957	. . . 4 |- (x = A -> (x e. B <-> A e. B))
5		eleq1 1957	. . . . 5 |- (x = A -> (x e. C <-> A e. C))
6	5	notbid 673	. . . 4 |- (x = A -> (-. x e. C <-> -. A e. C))
7	4, 6	anbi12d 690	. . 3 |- (x = A -> ((x e. B /\ -. x e. C) <-> (A e. B /\ -. A e. C)))
8		df-dif 2597	. . 3 |- (B \ C) = {x | (x e. B /\ -. x e. C)}
9	7, 8	elab2g 2406	. 2 |- (A e. _V -> (A e. (B \ C) <-> (A e. B /\ -. A e. C)))
10	1, 3, 9	pm5.21nii 743	1 |- (A e. (B \ C) <-> (A e. B /\ -. A e. C))

Syntax hints:  -. wn 2   <-> wb 163   /\ wa 240   = wceq 1298   e. wcel 1300  _Vcvv 2292   \ cdif 2590

This theorem is referenced by:  difeqri 2727  hbdif 2729  eldifi 2730  eldifn 2731  neldif 2733  difdif 2734  ddif 2737  ssconb 2738  sscon 2739  ssdif 2740  dfss4 2827  dfss4OLD 2828  dfun2 2829  dfin2 2830  difin 2831  difinOLD 2832  undif3 2854  symdif2 2857  symdif2OLD 2858  dfnul2 2877  reldisj 2916  reldisjOLD 2917  disj3 2918  undif4 2930  undif4OLD 2931  ssdif0 2934  pssnel 2938  difin0ss 2939  inssdif0 2940  inssdif0OLD 2941  inundif 2951  ssundif 2955  eldifsn 3123  difprsn 3127  iundif2 3322  iindif2 3324  brdif 3389  pwundif 3579  ordunidif 3712  onmindif 3760  eldifpw 3854  elpwunsn 3856  opelxpex2 4119  opelxpex2OLD 4120  intirr 4312  dfco2aOLD 4395  imadif 4493  dffv2 4734  oelim2 5270  oaabs 5309  brsdom 5440  brsdom2 5524  php3 5609  unblem1 5633  unfilem1 5641  infeq5 5727  kmlem4 5930  xrlenlt 6670  irradd 7457  irrmul 7458  modirr 7522  clsval2 8961  elcls 8980  islp2 9023  metelcls 9243  grothprim 10141  cdrci 10182  strlem1 11822  strlem5 11827  hstrlem5 11835  bnj158 12483  indifdi 13823  dif2relOLD 13828  dftr6 13834  wfi 13915  frind 13939  elsymdif 14062  brsset 14069  dfon3 14072  brbigcup 14074  ellimits 14079  difeqri2 14341  deref 14633  mlteqer 15017  subntr 15425  cptclsscpt 15432  hscptsscld 15434  alexsublem3 15439  locfincomp 15514  ist1-2 15542  fixufil 15576  ufinffr 15578  difin2 15676  difxp 15690  fdc 15812  recms 16010  isfldidl 16216  pridlc3 16221  prtlem80 16247  compel 16415  undif3VD 16706  strdif 16719  divrngidNEW 17166  iswatom 17394

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-dif 2597

Copyright terms: Public domain