Theorem eldifsn 3711

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 3131	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 3599	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 2381	. . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶))
4	3	pm5.32i 452	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
5	1, 4	bitri 183	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

Syntax hints:  ¬ wn 3   ∧ wa 103   ↔ wb 104   ∈ wcel 2142   ≠ wne 2341   ∖ cdif 3119  {csn 3584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 610  ax-in2 611  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-ext 2153

This theorem depends on definitions:  df-bi 116  df-tru 1352  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ne 2342  df-v 2733  df-dif 3124  df-sn 3590

This theorem is referenced by:  eldifsni  3713  rexdifsn  3716  difsn  3718  fnniniseg2  5623  rexsupp  5624  mpodifsnif  5950  suppssfv  6061  suppssov1  6062  dif1o  6421  fidifsnen  6852  en2eleq  7176  en2other2  7177  elni  7274  divvalap  8595  elnnne0  9153  divfnzn  9584  modfzo0difsn  10355  modsumfzodifsn  10356  hashdifpr  10759  eff2  11647  tanvalap  11675  fzo0dvdseq  11821  oddprmgt2  12092  oddprmdvds  12310  setsslnid  12471  grpinvnzcl  12775  rplogbval  13742  lgsfcl2  13786  lgsval2lem  13790  lgsval3  13798  lgsmod  13806  lgsdirprm  13814  lgsne0  13818