Theorem eldifsn 4317

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 3584	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 4191	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 2831	. . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶))
4	3	pm5.32i 669	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
5	1, 4	bitri 264	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 196   ∧ wa 384   ∈ wcel 1990   ≠ wne 2794   ∖ cdif 3571  {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-v 3202  df-dif 3577  df-sn 4178

This theorem is referenced by:  ssdifsn  4318  elpwdifsn  4319  eldifsni  4320  rexdifsn  4323  raldifsni  4324  eldifvsn  4326  difsn  4328  prproe  4434  sossfld  5580  tpres  6466  mpt2difsnif  6753  onmindif2  7012  mptsuppd  7318  suppssr  7326  suppssov1  7327  suppsssn  7330  suppssfv  7331  dif1o  7580  difsnen  8042  limenpsi  8135  frfi  8205  fofinf1o  8241  wemapso2lem  8457  en2eleq  8831  en2other2  8832  dfac8clem  8855  acni2  8869  acndom  8874  acnnum  8875  dfac9  8958  dfacacn  8963  kmlem3  8974  kmlem4  8975  fin23lem21  9161  canthp1lem2  9475  elni  9698  mulnzcnopr  10673  divval  10687  elnnne0  11306  elq  11790  rpcndif0  11851  modfzo0difsn  12742  modsumfzodifsn  12743  expcl2lem  12872  expclzlem  12884  hashdifpr  13203  prprrab  13255  hashle2prv  13260  reccn2  14327  rlimdiv  14376  eff2  14829  tanval  14858  rpnnen2lem9  14951  fzo0dvdseq  15045  oddprmgt2  15411  prmn2uzge3OLD  15413  oddprmdvds  15607  4sqlem19  15667  prmlem0  15812  prmlem1a  15813  setsnid  15915  grpinvnzcl  17487  symgextf  17837  symgextfv  17838  f1omvdmvd  17863  pmtrprfv  17873  odcau  18019  efgsf  18142  efgsrel  18147  efgs1  18148  efgs1b  18149  efgsp1  18150  efgsres  18151  efgredlema  18153  efgredlemd  18157  efgrelexlemb  18163  gsumpt  18361  dmdprdd  18398  dprdcntz  18407  dprdfeq0  18421  dprd2da  18441  drngunit  18752  isdrng2  18757  drngid2  18763  isdrngd  18772  issubdrg  18805  abvtriv  18841  islss  18935  lssneln0  18952  lssssr  18953  lbsind  19080  lbspss  19082  lspabs3  19121  lspsneq  19122  lspfixed  19128  lspexch  19129  islbs2  19154  isdomn2  19299  domnrrg  19300  mvrcl  19449  coe1tmmul2  19646  cnflddiv  19776  cnfldinv  19777  xrs1mnd  19784  xrs10  19785  xrge0subm  19787  cnsubdrglem  19797  cnmgpid  19808  cnmsubglem  19809  gzrngunit  19812  zringunit  19836  zringndrg  19838  domnchr  19880  cnmsgngrp  19925  psgninv  19928  psgndiflemB  19946  lindfind  20155  lindsind  20156  lindff1  20159  lindfrn  20160  mdetunilem9  20426  maducoeval2  20446  gsummatr01lem4  20464  ist1-2  21151  cmpfi  21211  2ndcdisj  21259  2ndcsep  21262  locfincmp  21329  alexsublem  21848  cldsubg  21914  imasdsf1olem  22178  prdsxmslem2  22334  reperflem  22621  xrge0gsumle  22636  xrge0tsms  22637  divcn  22671  evth  22758  cvsdiv  22932  cvsdivcl  22933  cphreccllem  22978  bcthlem5  23125  itg11  23458  i1fmullem  23461  i1fadd  23462  itg1addlem2  23464  i1fmulc  23470  itg1mulc  23471  ellimc3  23643  limcmpt2  23648  dvlem  23660  dvidlem  23679  dvcnp  23682  dvcobr  23709  dvrec  23718  dvrecg  23736  dvmptdiv  23737  dvcnvlem  23739  dvexp3  23741  dveflem  23742  dvferm1lem  23747  dvferm2lem  23749  lhop1lem  23776  ftc1lem5  23803  mdegleb  23824  coe1mul3  23859  ply1nz  23881  fta1blem  23928  fta1b  23929  ig1peu  23931  ig1pdvds  23936  plyeq0lem  23966  dgrub  23990  quotval  24047  fta1lem  24062  fta1  24063  elqaalem3  24076  qaa  24078  iaa  24080  aareccl  24081  aannenlem2  24084  abelthlem8  24193  abelth  24195  reefgim  24204  eff1olem  24294  logrncl  24314  eflog  24323  logeftb  24330  logdmss  24388  dvlog  24397  logbcl  24505  logbid1  24506  logb1  24507  elogb  24508  logbchbase  24509  relogbval  24510  relogbcl  24511  relogbreexp  24513  relogbmul  24515  nnlogbexp  24519  relogbcxp  24523  cxplogb  24524  relogbcxpb  24525  logbf  24527  logblog  24530  angval  24531  dcubic  24573  rlimcnp  24692  efrlim  24696  logexprlim  24950  dchrghm  24981  dchrabs  24985  lgsfcl2  25028  lgsval2lem  25032  lgsval3  25040  lgsmod  25048  lgsdirprm  25056  lgsne0  25060  gausslemma2dlem0f  25086  lgsquad2lem2  25110  2lgsoddprm  25141  2sqlem11  25154  2sqblem  25156  dchrvmaeq0  25193  rpvmasum2  25201  dchrisum0re  25202  qrngdiv  25313  tglngval  25446  tgisline  25522  axlowdimlem9  25830  axlowdimlem12  25833  axlowdimlem13  25834  upgrbi  25988  upgr1elem  26007  umgrislfupgrlem  26017  edgupgr  26029  subgruhgredgd  26176  upgrreslem  26196  nbgrel  26238  nbupgr  26240  nbupgrel  26241  nbumgrvtx  26242  nbgrssovtx  26260  nbupgrres  26266  nbusgrvtxm1uvtx  26306  nbupgruvtxres  26308  iscplgredg  26313  cusgredg  26320  cusgrfilem2  26352  usgredgsscusgredg  26355  1loopgrnb0  26398  1egrvtxdg0  26407  uhgrvd00  26430  vtxdginducedm1lem4  26438  eupth2lem3lem3  27090  frcond1  27130  frcond4  27134  2pthfrgr  27148  3cyclfrgrrn1  27149  n4cyclfrgr  27155  frgrwopreglem4a  27174  numclwwlk5  27246  suppss3  29502  xdivval  29627  xrge0tsmsd  29785  submatminr1  29876  ordtconnlem1  29970  ispisys2  30216  sigapisys  30218  sibfinima  30401  sseqf  30454  signswch  30638  signstfvn  30646  signsvtn0  30647  signstfvcl  30650  signstfveq0a  30653  signstfveq0  30654  signsvfn  30659  signsvtp  30660  signsvtn  30661  signsvfpn  30662  signsvfnn  30663  signlem0  30664  bnj158  30797  bnj168  30798  bnj529  30811  bnj906  31000  bnj970  31017  subfacp1lem5  31166  cvmsi  31247  cvmsval  31248  cvmsdisj  31252  cvmscld  31255  cvmsss2  31256  sinccvglem  31566  circum  31568  unbdqndv2lem2  32501  bj-0int  33055  lindsenlbs  33404  matunitlindflem2  33406  matunitlindf  33407  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem16  33425  poimirlem18  33427  poimirlem19  33428  poimirlem21  33430  poimirlem22  33431  poimirlem24  33433  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  itg2addnclem2  33462  sdclem1  33539  rrncmslem  33631  rrnequiv  33634  isdrngo2  33757  isdrngo3  33758  prtlem100  34144  prter2  34166  prter3  34167  lsatlspsn2  34279  lsateln0  34282  lsatn0  34286  lsatspn0  34287  lsatcmp  34290  lsatelbN  34293  islshpat  34304  lsat0cv  34320  lkrlspeqN  34458  dvheveccl  36401  dihlatat  36626  dochnel  36682  dihjat1  36718  dvh4dimlem  36732  dochsnkr2cl  36763  dochkr1  36767  dochkr1OLDN  36768  lcfl6lem  36787  lcfl9a  36794  lclkrlem2l  36807  lclkrlem2o  36810  lclkrlem2q  36812  lcfrlem9  36839  lcfrlem16  36847  lcfrlem17  36848  lcfrlem27  36858  lcfrlem37  36868  lcfrlem38  36869  lcfrlem40  36871  lcdlkreqN  36911  mapdrvallem2  36934  mapdn0  36958  mapdpglem20  36980  mapdpglem30  36991  mapdindp0  37008  mapdhcl  37016  mapdh6aN  37024  mapdh6dN  37028  mapdh6eN  37029  mapdh6kN  37035  mapdh8  37078  hdmap1l6a  37099  hdmap1l6d  37103  hdmap1l6e  37104  hdmap1l6k  37110  hdmapval3N  37130  hdmap10  37132  hdmap11lem2  37134  hdmapnzcl  37137  hdmaprnlem3eN  37150  hdmaprnlem17N  37155  hdmap14lem4a  37163  hdmap14lem7  37166  hdmap14lem14  37173  hgmaprnlem5N  37192  hdmaplkr  37205  hdmapip0  37207  hgmapvvlem2  37216  hgmapvvlem3  37217  hgmapvv  37218  pellexlem5  37397  dfac11  37632  dfacbasgrp  37678  dgraalem  37715  dgraaub  37718  aaitgo  37732  sdrgacs  37771  cntzsdrg  37772  proot1ex  37779  isdomn3  37782  deg1mhm  37785  ofdivrec  38525  ofdivcan4  38526  ofdivdiv2  38527  expgrowth  38534  binomcxplemnotnn0  38555  dvdivbd  40138  dvdivcncf  40142  dirkeritg  40319  fourierdlem39  40363  fourierdlem57  40380  fourierdlem58  40381  fourierdlem59  40382  fourierdlem68  40391  fourierdlem76  40399  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  setsnidel  41347  odz2prm2pw  41475  fmtnoprmfac1  41477  fmtnoprmfac2  41479  sfprmdvdsmersenne  41520  lighneallem2  41523  lighneallem3  41524  lighneal  41528  oddprmALTV  41598  evenprm2  41623  oddprmne2  41624  odd2prm2  41627  even3prm2  41628  sprvalpwn0  41733  2zrngnmrid  41950  fdmdifeqresdif  42120  lincext1  42243  lindslinindsimp2lem5  42251  rege1logbrege0  42352  fllogbd  42354  relogbmulbexp  42355  relogbdivb  42356  nnpw2blen  42374  blennngt2o2  42386  blennn0e2  42388  dignn0ldlem  42396  aacllem  42547