Theorem eldifsn 3774

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 3186	. 2 |- ( A e. ( B \ { C } ) <-> ( A e. B /\ -. A e. { C } ) )
2		elsng 3661	. . . 4 |- ( A e. B -> ( A e. { C } <-> A = C ) )
3	2	necon3bbid 2420	. . 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 2180   =/= wne 2380   \ cdif 3174   {csn 3646

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ne 2381  df-v 2781  df-dif 3179  df-sn 3652

This theorem is referenced by:  eldifsni  3776  rexdifsn  3779  difsn  3784  fnniniseg2  5731  rexsupp  5732  mpodifsnif  6068  suppssfv  6184  suppssov1  6185  dif1o  6554  fidifsnen  7000  en2eleq  7341  en2other2  7342  elni  7463  divvalap  8789  elnnne0  9351  divfnzn  9784  modfzo0difsn  10584  modsumfzodifsn  10585  hashdifpr  11009  eff2  12157  tanvalap  12185  fzo0dvdseq  12334  oddprmgt2  12622  oddprmdvds  12843  4sqlem19  12898  setsslnid  13050  grpinvnzcl  13571  lssneln0  14303  rplogbval  15584  lgsfcl2  15650  lgsval2lem  15654  lgsval3  15662  lgsmod  15670  lgsdirprm  15678  lgsne0  15682  gausslemma2dlem0f  15698  lgsquad2lem2  15726  2lgsoddprm  15757