Theorem eldifsn 4746

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 3921	. 2 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2		elsng 4599	. . . 4 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
3	2	necon3bbid 2962	. . 3 ⊢ (𝐴 ∈ 𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴 ≠ 𝐶))
4	3	pm5.32i 574	. 2 ⊢ ((𝐴 ∈ 𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))
5	1, 4	bitri 275	1 ⊢ (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ 𝐶))

Syntax hints:  ¬ wn 3   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   ≠ wne 2925   ∖ cdif 3908  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3446  df-dif 3914  df-sn 4586

This theorem is referenced by:  eldifsnd  4747  elpwdifsn  4749  eldifsni  4750  rexdifsn  4754  raldifsni  4755  eldifvsn  4757  difsn  4758  sossfld  6147  tpres  7157  onmindif2  7763  xpord3pred  8108  xpord3inddlem  8110  mptsuppd  8143  suppssr  8151  suppssov1  8153  suppssov2  8154  suppsssn  8157  suppssfv  8158  dif1o  8441  difsnen  9000  limenpsi  9093  frfi  9208  fofinf1o  9259  en2eleq  9939  en2other2  9940  dfac8clem  9963  acni2  9977  acndom  9982  acnnum  9983  dfac9  10068  dfacacn  10073  kmlem3  10084  kmlem4  10085  fin23lem21  10270  canthp1lem2  10584  elni  10807  mulnzcnf  11802  divval  11817  elnnne0  12434  elq  12887  rpcndif0  12950  modfzo0difsn  13886  modsumfzodifsn  13887  expcl2lem  14016  expclzlem  14026  hashdifpr  14358  hashgt23el  14367  prprrab  14416  hashle2prv  14421  reccn2  15540  rlimdiv  15589  eff2  16044  tanval  16073  rpnnen2lem9  16167  fzo0dvdseq  16270  oddprmgt2  16646  oddprmdvds  16851  4sqlem19  16911  prmlem0  17053  prmlem1a  17054  setsnid  17155  grpinvnzcl  18926  symgextf  19332  f1omvdmvd  19358  pmtrprfv  19368  odcau  19519  efgsf  19644  efgsrel  19649  efgs1  19650  efgs1b  19651  efgsp1  19652  efgsres  19653  efgredlema  19655  efgredlemd  19659  efgrelexlemb  19665  gsumpt  19877  dmdprdd  19916  dprdcntz  19925  dprdfeq0  19939  dprd2da  19959  isdomn2OLD  20633  domnrrg  20634  isdomn3  20636  drngunit  20655  isdrng2  20664  drngmcl  20671  drngid2  20673  isdrngd  20686  isdrngdOLD  20688  issubdrg  20701  sdrgacs  20722  cntzsdrg  20723  islss  20873  lssneln0  20892  lssssr  20893  lbsind  21020  lbspss  21022  lspabs3  21064  lspsneq  21065  lspfixed  21071  lspexch  21072  islbs2  21097  cnflddivOLD  21344  cnfldinv  21345  cnsubdrglem  21361  cnmgpid  21372  cnmsubglem  21373  gzrngunit  21376  xrs1mnd  21383  xrs10  21384  xrge0subm  21386  zringunit  21409  zringndrg  21411  domnchr  21475  cnmsgngrp  21522  psgninv  21525  psgndiflemB  21543  lindfind  21759  lindsind  21760  lindff1  21763  lindfrn  21764  mvrcl  21935  coe1tmmul2  22196  mdetunilem9  22541  maducoeval2  22561  gsummatr01lem4  22579  ist1-2  23268  cmpfi  23329  2ndcdisj  23377  2ndcsep  23380  locfincmp  23447  alexsublem  23965  cldsubg  24032  imasdsf1olem  24295  prdsxmslem2  24451  reperflem  24741  xrge0gsumle  24756  xrge0tsms  24757  divcnOLD  24791  divcn  24793  evth  24892  cvsdiv  25066  cvsdivcl  25067  cphreccllem  25112  bcthlem5  25262  itg11  25626  i1fmullem  25629  i1fadd  25630  itg1addlem2  25632  i1fmulc  25638  itg1mulc  25639  ellimc3  25814  limcmpt2  25819  dvlem  25831  dvidlem  25850  dvcnp  25854  dvcobr  25883  dvcobrOLD  25884  dvrec  25893  dvrecg  25911  dvmptdiv  25912  dvcnvlem  25914  dvexp3  25916  dveflem  25917  dvferm1lem  25922  dvferm2lem  25924  lhop1lem  25952  ftc1lem5  25981  mdegleb  26003  coe1mul3  26038  ply1nz  26061  fta1blem  26110  fta1b  26111  ig1peu  26114  ig1pdvds  26119  plyeq0lem  26149  dgrub  26173  quotval  26234  fta1lem  26249  fta1  26250  elqaalem3  26263  qaa  26265  iaa  26267  aareccl  26268  aannenlem2  26271  abelthlem8  26383  abelth  26385  eff1olem  26491  logrncl  26510  eflog  26519  logeftb  26526  logdmss  26585  dvlog  26594  logbcl  26711  logbid1  26712  logb1  26713  elogb  26714  logbchbase  26715  relogbval  26716  relogbcl  26717  relogbreexp  26719  relogbmul  26721  nnlogbexp  26725  relogbcxp  26729  cxplogb  26730  relogbcxpb  26731  logbf  26733  logblog  26736  2logb9irrALT  26742  sqrt2cxp2logb9e3  26743  angval  26745  dcubic  26790  rlimcnp  26909  efrlim  26913  efrlimOLD  26914  logexprlim  27170  dchrghm  27201  dchrabs  27205  lgsfcl2  27248  lgsval2lem  27252  lgsval3  27260  lgsmod  27268  lgsdirprm  27276  lgsne0  27280  gausslemma2dlem0f  27306  lgsquad2lem2  27330  2lgsoddprm  27361  2sqlem11  27374  2sqblem  27376  dchrvmaeq0  27449  rpvmasum2  27457  dchrisum0re  27458  qrngdiv  27569  addsval  27910  divsval  28133  elnns  28273  1nns  28282  tglngval  28532  tgisline  28608  axlowdimlem9  28931  axlowdimlem12  28934  axlowdimlem13  28935  elntg2  28966  upgrbi  29074  upgr1elem  29093  umgrislfupgrlem  29103  edgupgr  29115  subgruhgredgd  29265  upgrreslem  29285  nbgrel  29321  nbupgr  29325  nbupgrel  29326  nbumgrvtx  29327  nbgrssovtx  29342  nbupgrres  29345  nbusgrvtxm1uvtx  29386  nbupgruvtxres  29388  iscplgredg  29398  cusgredg  29405  cusgrfilem2  29438  usgredgsscusgredg  29441  1loopgrnb0  29484  1egrvtxdg0  29493  uhgrvd00  29516  vtxdginducedm1lem4  29524  eupth2lem3lem3  30210  frcond1  30246  frcond4  30250  2pthfrgr  30264  3cyclfrgrrn1  30265  n4cyclfrgr  30271  frgrwopreglem4a  30290  numclwwlk5  30368  ressupprn  32664  suppss3  32698  xdivval  32890  xrge0tsmsd  33046  pmtrcnel  33062  pmtrcnelor  33064  0nellinds  33335  dvdsruasso  33350  mxidlirredi  33436  extdg1id  33655  irngnzply1  33680  submatminr1  33794  ordtconnlem1  33908  ispisys2  34137  sigapisys  34139  sibfinima  34324  sseqf  34377  signswch  34546  signstfvn  34554  signsvtn0  34555  signstfvneq0  34557  signstfvcl  34558  signstfveq0a  34561  signstfveq0  34562  signsvfn  34567  signsvtp  34568  signsvtn  34569  signsvfpn  34570  signsvfnn  34571  signlem0  34572  bnj158  34713  bnj168  34714  bnj529  34725  bnj906  34914  bnj970  34931  exdifsn  35063  cusgredgex2  35104  subfacp1lem5  35165  cvmsi  35246  cvmsval  35247  cvmsdisj  35251  cvmscld  35254  cvmsss2  35255  satfv1lem  35343  sinccvglem  35653  circum  35655  mpomulnzcnf  36281  unbdqndv2lem2  36492  bj-0int  37083  lindsadd  37601  lindsenlbs  37603  matunitlindflem2  37605  matunitlindf  37606  poimirlem6  37614  poimirlem7  37615  poimirlem8  37616  poimirlem16  37624  poimirlem18  37626  poimirlem19  37627  poimirlem21  37629  poimirlem22  37630  poimirlem24  37632  poimirlem25  37633  poimirlem26  37634  poimirlem27  37635  itg2addnclem2  37660  sdclem1  37731  rrncmslem  37820  rrnequiv  37823  isdrngo2  37946  isdrngo3  37947  eldmxrncnvepres  38390  eldmxrncnvepres2  38391  prtlem100  38846  prter2  38868  prter3  38869  lsatlspsn2  38979  lsateln0  38982  lsatn0  38986  lsatspn0  38987  lsatcmp  38990  lsatelbN  38993  islshpat  39004  lsat0cv  39020  lkrlspeqN  39158  dvheveccl  41100  dihlatat  41325  dochnel  41381  dihjat1  41417  dvh4dimlem  41431  dochsnkr2cl  41462  dochkr1  41466  dochkr1OLDN  41467  lcfl6lem  41486  lcfl9a  41493  lclkrlem2l  41506  lclkrlem2o  41509  lclkrlem2q  41511  lcfrlem9  41538  lcfrlem16  41546  lcfrlem17  41547  lcfrlem27  41557  lcfrlem37  41567  lcfrlem38  41568  lcfrlem40  41570  lcdlkreqN  41610  mapdrvallem2  41633  mapdn0  41657  mapdpglem20  41679  mapdpglem30  41690  mapdindp0  41707  mapdhcl  41715  mapdh6aN  41723  mapdh6dN  41727  mapdh6eN  41728  mapdh6kN  41734  mapdh8  41776  hdmap1l6a  41797  hdmap1l6d  41801  hdmap1l6e  41802  hdmap1l6k  41808  hdmapval3N  41826  hdmap10  41828  hdmap11lem2  41830  hdmapnzcl  41833  hdmaprnlem3eN  41846  hdmaprnlem17N  41851  hdmap14lem4a  41859  hdmap14lem7  41862  hdmap14lem14  41869  hgmaprnlem5N  41888  hdmaplkr  41901  hdmapip0  41903  hgmapvvlem2  41912  hgmapvvlem3  41913  hgmapvv  41914  redvmptabs  42342  readvrec2  42343  readvrec  42344  fiabv  42518  fsuppind  42572  0prjspnlem  42605  pellexlem5  42815  dfac11  43045  dfacbasgrp  43091  dgraalem  43128  dgraaub  43131  aaitgo  43145  proot1ex  43179  deg1mhm  43183  ofdivrec  44309  ofdivcan4  44310  ofdivdiv2  44311  expgrowth  44318  binomcxplemnotnn0  44339  dvdivbd  45915  dvdivcncf  45919  dirkeritg  46094  fourierdlem39  46138  fourierdlem57  46155  fourierdlem58  46156  fourierdlem59  46157  fourierdlem68  46166  fourierdlem76  46174  fourierdlem103  46201  fourierdlem104  46202  fourierdlem111  46209  setsnidel  47372  sprvalpwn0  47478  odz2prm2pw  47558  fmtnoprmfac1  47560  fmtnoprmfac2  47562  sfprmdvdsmersenne  47598  lighneallem2  47601  lighneallem3  47602  lighneal  47606  oddprmALTV  47682  evenprm2  47709  oddprmne2  47710  odd2prm2  47713  even3prm2  47714  isubgruhgr  47862  grimuhgr  47881  2zrngnmrid  48238  lincext1  48437  lindslinindsimp2lem5  48445  rege1logbrege0  48541  fllogbd  48543  relogbmulbexp  48544  relogbdivb  48545  nnpw2blen  48563  blennngt2o2  48575  blennn0e2  48577  dignn0ldlem  48585  line  48715  rrxline  48717  aacllem  49784