Theorem eldifsn 4752

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209   ∧ wa 400   ∈ wcel 2142   ≠ wne 2957   ∖ cdif 3901  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-v 3456  df-dif 3907  df-sn 4589

This theorem is used by:  eldifsnbd  4753  eldifsnd  4754  eldifsni  4757  rexdifsn  4761  raldifsni  4762  eldifvsn  4764  difsn  4765  sossfld  6183  tpres  7199  onmindif2  7804  xpord3pred  8146  xpord3inddlem  8148  mptsuppd  8181  suppssr  8189  suppssov1  8191  suppssov2  8192  suppsssn  8195  suppssfv  8196  dif1o  8483  difsnen  9045  limenpsi  9138  frfi  9243  fofinf1o  9287  en2eleq  9999  en2other2  10000  dfac8clem  10023  acni2  10037  acndom  10042  acnnum  10043  dfac9  10127  dfacacn  10132  kmlem3  10143  kmlem4  10144  fin23lem21  10329  canthp1lem2  10644  elni  10867  mulnzcnf  11866  divval  11880  elnnne0  12524  elq  12980  rpcndif0  13043  modfzo0difsn  13986  modsumfzodifsn  13987  expcl2lem  14116  expclzlem  14126  hashdifpr  14459  hashgt23el  14468  prprrab  14517  hashle2prv  14522  reccn2  15655  rlimdiv  15704  eff2  16161  tanval  16190  rpnnen2lem9  16284  fzo0dvdseq  16387  oddprmgt2  16764  oddprmdvds  16969  4sqlem19  17029  prmlem0  17171  prmlem1a  17172  setsnid  17274  grpinvnzcl  19083  symgextf  19493  f1omvdmvd  19519  pmtrprfv  19529  odcau  19680  efgsf  19805  efgsrel  19810  efgs1  19811  efgs1b  19812  efgsp1  19813  efgsres  19814  efgredlema  19816  efgredlemd  19820  efgrelexlemb  19826  gsumpt  20038  dmdprdd  20077  dprdcntz  20086  dprdfeq0  20100  dprd2da  20120  domnrrg  20822  isdomn3  20824  drngunit  20843  isdrng2  20854  isdrng3lem2  20863  isdrng5  20865  drngmcl  20866  drngid2  20867  isdrngd  20879  isdrngdOLD  20881  issubdrg  20894  sdrgacs  20915  cntzsdrg  20916  islss  21066  lssneln0  21085  lssssr  21086  lbsind  21212  lbspss  21214  lspabs3  21256  lspsneq  21257  lspfixed  21263  lspexch  21264  islbs2  21289  cnfldinv  21564  cnsubdrglem  21579  cnmgpid  21590  cnmsubglem  21591  gzrngunit  21594  xrs1mnd  21601  xrs10  21602  xrge0subm  21604  zringunit  21627  zringndrg  21629  domnchr  21693  cnmsgngrp  21740  psgninv  21743  psgndiflemB  21761  lindfind  21977  lindsind  21978  lindff1  21981  lindfrn  21982  mvrcl  22152  coe1tmmul2  22448  mdetunilem9  22788  maducoeval2  22808  gsummatr01lem4  22826  ist1-2  23515  cmpfi  23576  2ndcdisj  23624  2ndcsep  23627  locfincmp  23694  alexsublem  24212  cldsubg  24279  imasdsf1olem  24541  prdsxmslem2  24697  reperflem  24987  xrge0gsumle  25002  xrge0tsms  25003  divcn  25038  evth  25129  cvsdiv  25302  cvsdivcl  25303  cphreccllem  25348  bcthlem5  25498  itg11  25861  i1fmullem  25864  i1fadd  25865  itg1addlem2  25867  i1fmulc  25873  itg1mulc  25874  ellimc3  26049  limcmpt2  26054  dvlem  26066  dvidlem  26085  dvcnp  26089  dvcobr  26116  dvrec  26125  dvrecg  26143  dvmptdiv  26144  dvcnvlem  26146  dvexp3  26148  dveflem  26149  dvferm1lem  26154  dvferm2lem  26156  lhop1lem  26183  ftc1lem5  26210  mdegleb  26232  coe1mul3  26267  ply1nz  26290  fta1blem  26339  fta1b  26340  ig1peu  26343  ig1pdvds  26348  plyeq0lem  26378  dgrub  26402  quotval  26464  fta1lem  26479  fta1  26480  elqaalem3  26493  qaa  26495  iaa  26499  aareccl  26500  aannenlem2  26503  abelthlem8  26613  abelth  26615  eff1olem  26724  logrncl  26743  eflog  26752  logeftb  26759  logdmss  26818  dvlog  26827  logbcl  26943  logbid1  26944  logb1  26945  elogb  26946  logbchbase  26947  relogbval  26948  relogbcl  26949  relogbreexp  26951  relogbmul  26953  nnlogbexp  26957  relogbcxp  26961  cxplogb  26962  relogbcxpb  26963  logbf  26965  logblog  26968  2logb9irrALT  26974  sqrt2cxp2logb9e3  26975  angval  26977  dcubic  27022  rlimcnp  27141  efrlim  27145  logexprlim  27400  dchrghm  27431  dchrabs  27435  lgsfcl2  27478  lgsval2lem  27482  lgsval3  27490  lgsmod  27498  lgsdirprm  27506  lgsne0  27510  gausslemma2dlem0f  27536  lgsquad2lem2  27560  2lgsoddprm  27591  2sqlem11  27604  2sqblem  27606  dchrvmaeq0  27679  rpvmasum2  27687  dchrisum0re  27688  qrngdiv  27799  addsval  28166  divsval  28393  elnns  28544  1nns  28553  tglngval  28831  tgisline  28911  axlowdimlem9  29311  axlowdimlem12  29314  axlowdimlem13  29315  elntg2  29346  upgrbi  29454  upgr1elem  29473  umgrislfupgrlem  29483  edgupgr  29495  subgruhgredgd  29645  upgrreslem  29665  nbgrel  29701  nbupgr  29705  nbupgrel  29706  nbumgrvtx  29707  nbgrssovtx  29722  nbupgrres  29725  nbusgrvtxm1uvtx  29766  nbupgruvtxres  29768  iscplgredg  29778  cusgredg  29785  cusgrfilem2  29817  usgredgsscusgredg  29820  1loopgrnb0  29863  1egrvtxdg0  29872  uhgrvd00  29895  vtxdginducedm1lem4  29903  eupth2lem3lem3  30592  frcond1  30628  frcond4  30632  2pthfrgr  30646  3cyclfrgrrn1  30647  n4cyclfrgr  30653  frgrwopreglem4a  30672  numclwwlk5  30750  ressupprn  33046  suppss3  33079  xdivval  33249  xrge0tsmsd  33402  pmtrcnel  33418  pmtrcnelor  33420  0nellinds  33694  dvdsruasso  33707  extdg1id  34065  irngnzply1  34090  submatminr1  34209  ordtconnlem1  34323  ispisys2  34552  sigapisys  34554  sibfinima  34738  sseqf  34791  signswch  34957  signstfvn  34965  signsvtn0  34966  signstfvneq0  34968  signstfvcl  34969  signstfveq0a  34972  signstfveq0  34973  signsvfn  34978  signsvtp  34979  signsvtn  34980  signsvfpn  34981  signsvfnn  34982  signlem0  34983  bnj158  35127  bnj168  35128  bnj529  35139  bnj906  35327  bnj970  35344  exdifsn  35477  cusgredgex2  35623  subfacp1lem5  35684  cvmsi  35765  cvmsval  35766  cvmsdisj  35770  cvmscld  35773  cvmsss2  35774  satfv1lem  35862  sinccvglem  36172  circum  36174  mpomulnzcnf  36839  unbdqndv2lem2  37127  bj-0int  37771  lindsadd  38292  lindsenlbs  38294  matunitlindflem2  38296  matunitlindf  38297  poimirlem6  38305  poimirlem7  38306  poimirlem8  38307  poimirlem16  38315  poimirlem18  38317  poimirlem19  38318  poimirlem21  38320  poimirlem22  38321  poimirlem24  38323  poimirlem25  38324  poimirlem26  38325  poimirlem27  38326  itg2addnclem2  38351  sdclem1  38422  rrncmslem  38511  rrnequiv  38514  isdrngo2  38637  isdrngo3  38638  eldmxrncnvepres  39111  eldmxrncnvepres2  39112  prtlem100  39661  prter2  39683  prter3  39684  lsatlspsn2  39794  lsateln0  39797  lsatn0  39801  lsatspn0  39802  lsatcmp  39805  lsatelbN  39808  islshpat  39819  lsat0cv  39835  lkrlspeqN  39973  dvheveccl  41914  dihlatat  42139  dochnel  42195  dihjat1  42231  dvh4dimlem  42245  dochsnkr2cl  42276  dochkr1  42280  dochkr1OLDN  42281  lcfl6lem  42300  lcfl9a  42307  lclkrlem2l  42320  lclkrlem2o  42323  lclkrlem2q  42325  lcfrlem9  42352  lcfrlem16  42360  lcfrlem17  42361  lcfrlem27  42371  lcfrlem37  42381  lcfrlem38  42382  lcfrlem40  42384  lcdlkreqN  42424  mapdrvallem2  42447  mapdn0  42471  mapdpglem20  42493  mapdpglem30  42504  mapdindp0  42521  mapdhcl  42529  mapdh6aN  42537  mapdh6dN  42541  mapdh6eN  42542  mapdh6kN  42548  mapdh8  42590  hdmap1l6a  42611  hdmap1l6d  42615  hdmap1l6e  42616  hdmap1l6k  42622  hdmapval3N  42640  hdmap10  42642  hdmap11lem2  42644  hdmapnzcl  42647  hdmaprnlem3eN  42660  hdmaprnlem17N  42665  hdmap14lem4a  42673  hdmap14lem7  42676  hdmap14lem14  42683  hgmaprnlem5N  42702  hdmaplkr  42715  hdmapip0  42717  hgmapvvlem2  42726  hgmapvvlem3  42727  hgmapvv  42728  redvmptabs  43149  readvrec2  43150  readvrec  43151  fiabv  43332  fsuppind  43350  0prjspnlem  43383  pellexlem5  43588  dfac11  43817  dfacbasgrp  43863  dgraalem  43900  dgraaub  43903  aaitgo  43917  proot1ex  43951  deg1mhm  43955  ofdivrec  45064  ofdivcan4  45065  ofdivdiv2  45066  expgrowth  45073  binomcxplemnotnn0  45094  dvdivbd  46665  dvdivcncf  46669  dirkeritg  46844  fourierdlem39  46888  fourierdlem57  46905  fourierdlem58  46906  fourierdlem59  46907  fourierdlem68  46916  fourierdlem76  46924  fourierdlem103  46951  fourierdlem104  46952  fourierdlem111  46959  sqrtnnaa  47632  setsnidel  48154  sprvalpwn0  48260  odz2prm2pw  48343  fmtnoprmfac1  48345  fmtnoprmfac2  48347  sfprmdvdsmersenne  48383  lighneallem2  48386  lighneallem3  48387  lighneal  48391  oddprmALTV  48480  evenprm2  48507  oddprmne2  48508  odd2prm2  48511  even3prm2  48512  isubgruhgr  48661  grimuhgr  48680  2zrngnmrid  49049  lincext1  49262  lindslinindsimp2lem5  49270  rege1logbrege0  49366  fllogbd  49368  relogbmulbexp  49369  relogbdivb  49370  nnpw2blen  49388  blennngt2o2  49400  blennn0e2  49402  dignn0ldlem  49410  line  49540  rrxline  49542  aacllem  50649