Theorem eldifsn 3819

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 3219	. 2 |- ( A e. ( B \ { C } ) <-> ( A e. B /\ -. A e. { C } ) )
2		elsng 3703	. . . 4 |- ( A e. B -> ( A e. { C } <-> A = C ) )
3	2	necon3bbid 2452	. . 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 2203   =/= wne 2412   \ cdif 3207   {csn 3688

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-v 2814  df-dif 3212  df-sn 3694

This theorem is referenced by:  eldifsni  3821  rexdifsn  3824  eldifvsn  3825  difsn  3830  fnniniseg2  5800  mpodifsnif  6145  suppssov1  6262  mptsuppd  6455  suppssrst  6460  suppssrgst  6461  suppssfvg  6462  dif1o  6670  fidifsnen  7124  en2eleq  7497  en2other2  7498  elni  7619  divvalap  8944  elnnne0  9506  divfnzn  9949  modfzo0difsn  10753  modsumfzodifsn  10754  hashdifpr  11180  eff2  12359  tanvalap  12387  fzo0dvdseq  12536  oddprmgt2  12824  oddprmdvds  13045  4sqlem19  13100  setsslnid  13253  grpinvnzcl  13774  lssneln0  14509  rplogbval  15797  lgsfcl2  15866  lgsval2lem  15870  lgsval3  15878  lgsmod  15886  lgsdirprm  15894  lgsne0  15898  gausslemma2dlem0f  15914  lgsquad2lem2  15942  2lgsoddprm  15973  eupth2lem3lem3fi  16452