Theorem eldifsn 3800

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

Assertion

Ref	Expression
eldifsn	⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

Proof of Theorem eldifsn

Step	Hyp	Ref	Expression
1		eldif 3209	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 3684	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 2442	. . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶))
4	3	pm5.32i 454	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
5	1, 4	bitri 184	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

Syntax hints:  ¬ wn 3   ∧ wa 104   ↔ wb 105   ∈ wcel 2202   ≠ wne 2402   ∖ cdif 3197  {csn 3669

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-v 2804  df-dif 3202  df-sn 3675

This theorem is referenced by:  eldifsni  3802  rexdifsn  3805  difsn  3810  fnniniseg2  5770  rexsupp  5771  mpodifsnif  6114  suppssfv  6231  suppssov1  6232  dif1o  6606  fidifsnen  7057  en2eleq  7406  en2other2  7407  elni  7528  divvalap  8854  elnnne0  9416  divfnzn  9855  modfzo0difsn  10658  modsumfzodifsn  10659  hashdifpr  11085  eff2  12243  tanvalap  12271  fzo0dvdseq  12420  oddprmgt2  12708  oddprmdvds  12929  4sqlem19  12984  setsslnid  13136  grpinvnzcl  13657  lssneln0  14391  rplogbval  15672  lgsfcl2  15738  lgsval2lem  15742  lgsval3  15750  lgsmod  15758  lgsdirprm  15766  lgsne0  15770  gausslemma2dlem0f  15786  lgsquad2lem2  15814  2lgsoddprm  15845  eupth2lem3lem3fi  16324