Theorem eldifsn 4748

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 3909	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 4598	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 2992	. . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶))
4	3	pm5.32i 585	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
5	1, 4	bitri 278	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 401   ∈ wcel 2145   ≠ wne 2955   ∖ cdif 3896  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-dif 3902  df-sn 4585

This theorem is used by:  eldifsnbd  4749  eldifsnd  4750  eldifsni  4753  rexdifsn  4757  raldifsni  4758  eldifvsn  4760  difsn  4761  sossfld  6174  tpres  7196  onmindif2  7805  xpord3pred  8148  xpord3inddlem  8150  mptsuppd  8183  suppssr  8191  suppssov1  8193  suppssov2  8194  suppsssn  8197  suppssfv  8198  dif1o  8487  difsnen  9057  limenpsi  9150  frfi  9255  fofinf1o  9299  en2eleq  10044  en2other2  10045  dfac8clem  10068  acni2  10082  acndom  10087  acnnum  10088  dfac9  10172  dfacacn  10177  kmlem3  10188  kmlem4  10189  fin23lem21  10374  canthp1lem2  10695  elni  10918  mulnzcnf  11917  divval  11931  elnnne0  12575  elq  13032  rpcndif0  13096  modfzo0difsn  14040  modsumfzodifsn  14041  expcl2lem  14170  expclzlem  14180  hashdifpr  14513  hashgt23el  14522  prprrab  14571  hashle2prv  14576  reccn2  15717  rlimdiv  15766  eff2  16220  tanval  16249  rpnnen2lem9  16343  fzo0dvdseq  16446  oddprmgt2  16823  oddprmdvds  17028  4sqlem19  17088  prmlem0  17230  prmlem1a  17231  setsnid  17333  grpinvnzcl  19168  symgextf  19578  f1omvdmvd  19604  pmtrprfv  19614  odcau  19765  efgsf  19890  efgsrel  19895  efgs1  19896  efgs1b  19897  efgsp1  19898  efgsres  19899  efgredlema  19901  efgredlemd  19905  efgrelexlemb  19911  gsumpt  20123  dmdprdd  20162  dprdcntz  20171  dprdfeq0  20185  dprd2da  20205  domnrrg  20911  isdomn3  20913  drngunit  20932  isdrng3lem2  20953  isdrng5  20955  drngmcl  20956  drngid2  20957  isdrngd  20969  isdrngdOLD  20971  issubdrg  20984  sdrgacs  21005  cntzsdrg  21006  islss  21156  lssneln0  21175  lssssr  21176  lbsind  21302  lbspss  21304  lspabs3  21346  lspsneq  21347  lspfixed  21353  lspexch  21354  islbs2  21379  cnfldinv  21656  cnsubdrglem  21671  cnmgpid  21682  cnmsubglem  21683  gzrngunit  21686  xrs1mnd  21693  xrs10  21694  xrge0subm  21696  zringunit  21719  zringndrg  21721  domnchr  21785  cnmsgngrp  21832  psgninv  21835  psgndiflemB  21853  lindfind  22069  lindsind  22070  lindff1  22073  lindfrn  22074  lindsenlbs  22104  mvrcl  22246  coe1tmmul2  22542  mdetunilem9  22882  maducoeval2  22902  gsummatr01lem4  22920  matunitlindflem2  22942  matunitlindf  22943  ist1-2  23612  cmpfi  23673  2ndcdisj  23722  2ndcsep  23725  locfincmp  23792  alexsublem  24310  cldsubg  24377  imasdsf1olem  24639  prdsxmslem2  24795  reperflem  25085  xrge0gsumle  25100  xrge0tsms  25101  divcn  25136  evth  25227  cvsdiv  25400  cvsdivcl  25401  cphreccllem  25446  bcthlem5  25596  itg11  25959  i1fmullem  25962  i1fadd  25963  itg1addlem2  25965  i1fmulc  25971  itg1mulc  25972  ellimc3  26146  limcmpt2  26151  dvlem  26163  dvidlem  26182  dvcnp  26186  dvcobr  26213  dvrec  26222  dvrecg  26240  dvmptdiv  26241  dvcnvlem  26243  dvexp3  26245  dveflem  26246  dvferm1lem  26251  dvferm2lem  26253  lhop1lem  26280  ftc1lem5  26307  mdegleb  26329  coe1mul3  26364  ply1nz  26387  fta1blem  26436  fta1b  26437  ig1peu  26440  ig1pdvds  26445  plyeq0lem  26476  dgrub  26500  quotval  26562  fta1lem  26577  fta1  26578  elqaalem3  26593  qaa  26596  iaaOLD  26601  aareccl  26602  aannenlem2  26605  abelthlem8  26715  abelth  26717  eff1olem  26825  logrncl  26844  eflog  26853  logeftb  26860  logdmss  26919  dvlog  26928  logbcl  27044  logbid1  27045  logb1  27046  elogb  27047  logbchbase  27048  relogbval  27049  relogbcl  27050  relogbreexp  27052  relogbmul  27054  nnlogbexp  27058  relogbcxp  27062  cxplogb  27063  relogbcxpb  27064  logbf  27066  logblog  27069  2logb9irrALT  27075  sqrt2cxp2logb9e3  27076  angval  27078  dcubic  27123  rlimcnp  27242  efrlim  27246  logexprlim  27501  dchrghm  27532  dchrabs  27536  lgsfcl2  27579  lgsval2lem  27583  lgsval3  27591  lgsmod  27599  lgsdirprm  27607  lgsne0  27611  gausslemma2dlem0f  27637  lgsquad2lem2  27661  2lgsoddprm  27692  2sqlem11  27705  2sqblem  27707  dchrvmaeq0  27780  rpvmasum2  27788  dchrisum0re  27789  qrngdiv  27900  addsval  28267  divsval  28494  elnns  28645  1nns  28654  tglngval  28933  tgisline  29014  axlowdimlem9  29447  axlowdimlem12  29450  axlowdimlem13  29451  elntg2  29482  upgrbi  29590  upgr1elem  29609  umgrislfupgrlem  29619  edgupgr  29631  subgruhgredgd  29784  upgrreslem  29804  nbgrel  29840  nbupgr  29844  nbupgrel  29845  nbumgrvtx  29846  nbgrssovtx  29861  nbupgrres  29864  nbusgrvtxm1uvtx  29905  nbupgruvtxres  29907  iscplgredg  29917  cusgredg  29924  cusgrfilem2  29956  usgredgsscusgredg  29959  1loopgrnb0  30002  1egrvtxdg0  30011  uhgrvd00  30034  vtxdginducedm1lem4  30042  eupth2lem3lem3  30750  frcond1  30786  frcond4  30790  2pthfrgr  30804  3cyclfrgrrn1  30805  n4cyclfrgr  30811  frgrwopreglem4a  30830  numclwwlk5  30908  ressupprn  33202  suppss3  33234  xdivval  33404  xrge0tsmsd  33553  pmtrcnel  33569  pmtrcnelor  33571  0nellinds  33845  dvdsruasso  33859  extdg1id  34217  irngnzply1  34242  submatminr1  34361  ordtconnlem1  34475  ispisys2  34705  sigapisys  34707  sibfinima  34891  sseqf  34944  signswch  35110  signstfvn  35118  signsvtn0  35119  signstfvneq0  35121  signstfvcl  35122  signstfveq0a  35125  signstfveq0  35126  signsvfn  35131  signsvtp  35132  signsvtn  35133  signsvfpn  35134  signsvfnn  35135  signlem0  35136  bnj158  35280  bnj168  35281  bnj529  35292  bnj906  35480  bnj970  35497  exdifsn  35630  cusgredgex2  35822  subfacp1lem5  35864  cvmsi  35945  cvmsval  35946  cvmsdisj  35950  cvmscld  35953  cvmsss2  35954  satfv1lem  36042  sinccvglem  36352  circum  36354  mpomulnzcnf  37004  unbdqndv2lem2  37292  bj-0int  37936  lindsadd  38450  poimirlem6  38458  poimirlem7  38459  poimirlem8  38460  poimirlem16  38468  poimirlem18  38470  poimirlem19  38471  poimirlem21  38473  poimirlem22  38474  poimirlem24  38476  poimirlem25  38477  poimirlem26  38478  poimirlem27  38479  itg2addnclem2  38504  sdclem1  38591  rrncmslem  38680  rrnequiv  38683  isdrngo2  38806  isdrngo3  38807  eldmxrncnvepres  39280  eldmxrncnvepres2  39281  prtlem100  39830  prter2  39852  prter3  39853  lsatlspsn2  39963  lsateln0  39966  lsatn0  39970  lsatspn0  39971  lsatcmp  39974  lsatelbN  39977  islshpat  39988  lsat0cv  40004  lkrlspeqN  40142  dvheveccl  42083  dihlatat  42308  dochnel  42364  dihjat1  42400  dvh4dimlem  42414  dochsnkr2cl  42445  dochkr1  42449  dochkr1OLDN  42450  lcfl6lem  42469  lcfl9a  42476  lclkrlem2l  42489  lclkrlem2o  42492  lclkrlem2q  42494  lcfrlem9  42521  lcfrlem16  42529  lcfrlem17  42530  lcfrlem27  42540  lcfrlem37  42550  lcfrlem38  42551  lcfrlem40  42553  lcdlkreqN  42593  mapdrvallem2  42616  mapdn0  42640  mapdpglem20  42662  mapdpglem30  42673  mapdindp0  42690  mapdhcl  42698  mapdh6aN  42706  mapdh6dN  42710  mapdh6eN  42711  mapdh6kN  42717  mapdh8  42759  hdmap1l6a  42780  hdmap1l6d  42784  hdmap1l6e  42785  hdmap1l6k  42791  hdmapval3N  42809  hdmap10  42811  hdmap11lem2  42813  hdmapnzcl  42816  hdmaprnlem3eN  42829  hdmaprnlem17N  42834  hdmap14lem4a  42842  hdmap14lem7  42845  hdmap14lem14  42852  hgmaprnlem5N  42871  hdmaplkr  42884  hdmapip0  42886  hgmapvvlem2  42895  hgmapvvlem3  42896  hgmapvv  42897  redvmptabs  43333  readvrec2  43334  readvrec  43335  fiabv  43516  fsuppind  43534  0prjspnlem  43567  pellexlem5  43772  dfac11  44001  dfacbasgrp  44047  dgraalem  44084  dgraaub  44087  aaitgo  44101  proot1ex  44135  deg1mhm  44139  ofdivrec  45248  ofdivcan4  45249  ofdivdiv2  45250  expgrowth  45257  binomcxplemnotnn0  45278  dvdivbd  46849  dvdivcncf  46853  dirkeritg  47028  fourierdlem39  47072  fourierdlem57  47089  fourierdlem58  47090  fourierdlem59  47091  fourierdlem68  47100  fourierdlem76  47108  fourierdlem103  47135  fourierdlem104  47136  fourierdlem111  47143  setsnidel  48375  sprvalpwn0  48481  odz2prm2pw  48564  fmtnoprmfac1  48566  fmtnoprmfac2  48568  sfprmdvdsmersenne  48604  lighneallem2  48607  lighneallem3  48608  lighneal  48612  oddprmALTV  48701  evenprm2  48728  oddprmne2  48729  odd2prm2  48732  even3prm2  48733  isubgruhgr  48882  grimuhgr  48901  2zrngnmrid  49269  lincext1  49482  lindslinindsimp2lem5  49490  rege1logbrege0  49586  fllogbd  49588  relogbmulbexp  49589  relogbdivb  49590  nnpw2blen  49608  blennngt2o2  49620  blennn0e2  49622  dignn0ldlem  49630  line  49760  rrxline  49762  dvsec  50772  dvcsc  50773  dvcot  50774  aacllem  50855  veroquadmodzerod  50900  veroquadnolindfd  50901