Theorem eldifsn 3795

Description: Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)

Assertion

Ref	Expression
eldifsn	|- ( A e. ( B \ { C } ) <-> ( A e. B /\ A =/= C ) )

Proof of Theorem eldifsn

Step	Hyp	Ref	Expression
1		eldif 3206	. 2 |- ( A e. ( B \ { C } ) <-> ( A e. B /\ -. A e. { C } ) )
2		elsng 3681	. . . 4 |- ( A e. B -> ( A e. { C } <-> A = C ) )
3	2	necon3bbid 2440	. . 3 |- ( A e. B -> ( -. A e. { C } <-> A =/= C ) )
4	3	pm5.32i 454	. 2 |- ( ( A e. B /\ -. A e. { C } ) <-> ( A e. B /\ A =/= C ) )
5	1, 4	bitri 184	1 |- ( A e. ( B \ { C } ) <-> ( A e. B /\ A =/= C ) )

Syntax hints:   -. wn 3   /\ wa 104   <-> wb 105   e. wcel 2200   =/= wne 2400   \ cdif 3194   {csn 3666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-v 2801  df-dif 3199  df-sn 3672

This theorem is referenced by:  eldifsni  3797  rexdifsn  3800  difsn  3805  fnniniseg2  5763  rexsupp  5764  mpodifsnif  6106  suppssfv  6223  suppssov1  6224  dif1o  6597  fidifsnen  7045  en2eleq  7389  en2other2  7390  elni  7511  divvalap  8837  elnnne0  9399  divfnzn  9833  modfzo0difsn  10634  modsumfzodifsn  10635  hashdifpr  11060  eff2  12212  tanvalap  12240  fzo0dvdseq  12389  oddprmgt2  12677  oddprmdvds  12898  4sqlem19  12953  setsslnid  13105  grpinvnzcl  13626  lssneln0  14359  rplogbval  15640  lgsfcl2  15706  lgsval2lem  15710  lgsval3  15718  lgsmod  15726  lgsdirprm  15734  lgsne0  15738  gausslemma2dlem0f  15754  lgsquad2lem2  15782  2lgsoddprm  15813