Theorem eldif 3222

Description: Membership in difference. (Contributed by SF, 10-Jan-2015.)

Assertion

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

Proof of Theorem eldif

Step	Hyp	Ref	Expression
1		df-dif 3216	. . 3 |- (B \ C) = (B i^i ∼ C)
2	1	eleq2i 2417	. 2 |- (A e. (B \ C) <-> A e. (B i^i ∼ C))
3		elin 3220	. 2 |- (A e. (B i^i ∼ C) <-> (A e. B /\ A e. ∼ C))
4		elcomplg 3219	. . 3 |- (A e. B -> (A e. ∼ C <-> -. A e. C))
5	4	pm5.32i 618	. 2 |- ((A e. B /\ A e. ∼ C) <-> (A e. B /\ -. A e. C))
6	2, 3, 5	3bitri 262	1 |- (A e. (B \ C) <-> (A e. B /\ -. A e. C))

Syntax hints:  -. wn 3   <-> wb 176   /\ wa 358   e. wcel 1710   ∼ ccompl 3206   \ cdif 3207   i^i cin 3209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-dif 3216

This theorem is referenced by:  dfdif2  3223  elsymdif  3224  difeqri  3388  eldifi  3389  eldifn  3390  neldif  3392  difdif  3393  ddif  3399  ssconb  3400  sscon  3401  ssdif  3402  dfss4  3490  dfun2  3491  dfin2  3492  difin  3493  indifdir  3512  undif3  3516  difin2  3517  symdif2  3521  dfnul2  3553  reldisj  3595  disj3  3596  undif4  3608  ssdif0  3610  pssnel  3616  difin0ss  3617  inssdif0  3618  inundif  3629  ssundif  3634  eldifsn  3840  difprsnss  3847  iundif2  4034  iindif2  4036  opkelimagekg  4272  dfpw2  4328  dfaddc2  4382  dfnnc2  4396  nnsucelrlem1  4425  nnsucelr  4429  ltfinex  4465  ssfin  4471  eqpw1relk  4480  ncfinraiselem2  4481  ncfinlowerlem1  4483  eqtfinrelk  4487  evenodddisjlem1  4516  nnadjoinlem1  4520  nnpweqlem1  4523  sfintfinlem1  4532  tfinnnlem1  4534  spfinex  4538  brdif  4695  cnvdif  5035  imadif  5172  releqmpt2  5810  funsex  5829  transex  5911  antisymex  5913  connexex  5914  foundex  5915  extex  5916  symex  5917  2p1e3c  6157  nchoicelem11  6300  nchoicelem16  6305  fnfreclem1  6318