Theorem eldifsn 3746

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 3163	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 3634	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 2404	. . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶))
4	3	pm5.32i 454	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
5	1, 4	bitri 184	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

Syntax hints:  ¬ wn 3   ∧ wa 104   ↔ wb 105   ∈ wcel 2164   ≠ wne 2364   ∖ cdif 3151  {csn 3619

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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-v 2762  df-dif 3156  df-sn 3625

This theorem is referenced by:  eldifsni  3748  rexdifsn  3751  difsn  3756  fnniniseg2  5682  rexsupp  5683  mpodifsnif  6012  suppssfv  6128  suppssov1  6129  dif1o  6493  fidifsnen  6928  en2eleq  7257  en2other2  7258  elni  7370  divvalap  8695  elnnne0  9257  divfnzn  9689  modfzo0difsn  10469  modsumfzodifsn  10470  hashdifpr  10894  eff2  11826  tanvalap  11854  fzo0dvdseq  12002  oddprmgt2  12275  oddprmdvds  12495  4sqlem19  12550  setsslnid  12673  grpinvnzcl  13147  lssneln0  13873  rplogbval  15118  lgsfcl2  15163  lgsval2lem  15167  lgsval3  15175  lgsmod  15183  lgsdirprm  15191  lgsne0  15195  gausslemma2dlem0f  15211  lgsquad2lem2  15239  2lgsoddprm  15270