Theorem eldifsn 3801

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

Syntax hints:  ¬ wn 3   ∧ wa 104   ↔ wb 105   ∈ wcel 2201   ≠ wne 2401   ∖ cdif 3196  {csn 3670

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 2212

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-ne 2402  df-v 2803  df-dif 3201  df-sn 3676

This theorem is referenced by:  eldifsni  3803  rexdifsn  3806  difsn  3811  fnniniseg2  5773  rexsupp  5774  mpodifsnif  6119  suppssfv  6236  suppssov1  6237  dif1o  6611  fidifsnen  7062  en2eleq  7411  en2other2  7412  elni  7533  divvalap  8859  elnnne0  9421  divfnzn  9860  modfzo0difsn  10663  modsumfzodifsn  10664  hashdifpr  11090  eff2  12264  tanvalap  12292  fzo0dvdseq  12441  oddprmgt2  12729  oddprmdvds  12950  4sqlem19  13005  setsslnid  13157  grpinvnzcl  13678  lssneln0  14412  rplogbval  15698  lgsfcl2  15764  lgsval2lem  15768  lgsval3  15776  lgsmod  15784  lgsdirprm  15792  lgsne0  15796  gausslemma2dlem0f  15812  lgsquad2lem2  15840  2lgsoddprm  15871  eupth2lem3lem3fi  16350