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  9937  en2other2  9938  dfac8clem  9961  acni2  9975  acndom  9980  acnnum  9981  dfac9  10066  dfacacn  10071  kmlem3  10082  kmlem4  10083  fin23lem21  10268  canthp1lem2  10582  elni  10805  mulnzcnf  11800  divval  11815  elnnne0  12432  elq  12885  rpcndif0  12948  modfzo0difsn  13884  modsumfzodifsn  13885  expcl2lem  14014  expclzlem  14024  hashdifpr  14356  hashgt23el  14365  prprrab  14414  hashle2prv  14419  reccn2  15539  rlimdiv  15588  eff2  16043  tanval  16072  rpnnen2lem9  16166  fzo0dvdseq  16269  oddprmgt2  16645  oddprmdvds  16850  4sqlem19  16910  prmlem0  17052  prmlem1a  17053  setsnid  17154  grpinvnzcl  18925  symgextf  19331  f1omvdmvd  19357  pmtrprfv  19367  odcau  19518  efgsf  19643  efgsrel  19648  efgs1  19649  efgs1b  19650  efgsp1  19651  efgsres  19652  efgredlema  19654  efgredlemd  19658  efgrelexlemb  19664  gsumpt  19876  dmdprdd  19915  dprdcntz  19924  dprdfeq0  19938  dprd2da  19958  isdomn2OLD  20632  domnrrg  20633  isdomn3  20635  drngunit  20654  isdrng2  20663  drngmcl  20670  drngid2  20672  isdrngd  20685  isdrngdOLD  20687  issubdrg  20700  sdrgacs  20721  cntzsdrg  20722  islss  20872  lssneln0  20891  lssssr  20892  lbsind  21019  lbspss  21021  lspabs3  21063  lspsneq  21064  lspfixed  21070  lspexch  21071  islbs2  21096  cnflddivOLD  21343  cnfldinv  21344  cnsubdrglem  21360  cnmgpid  21371  cnmsubglem  21372  gzrngunit  21375  xrs1mnd  21382  xrs10  21383  xrge0subm  21385  zringunit  21408  zringndrg  21410  domnchr  21474  cnmsgngrp  21521  psgninv  21524  psgndiflemB  21542  lindfind  21758  lindsind  21759  lindff1  21762  lindfrn  21763  mvrcl  21934  coe1tmmul2  22195  mdetunilem9  22540  maducoeval2  22560  gsummatr01lem4  22578  ist1-2  23267  cmpfi  23328  2ndcdisj  23376  2ndcsep  23379  locfincmp  23446  alexsublem  23964  cldsubg  24031  imasdsf1olem  24294  prdsxmslem2  24450  reperflem  24740  xrge0gsumle  24755  xrge0tsms  24756  divcnOLD  24790  divcn  24792  evth  24891  cvsdiv  25065  cvsdivcl  25066  cphreccllem  25111  bcthlem5  25261  itg11  25625  i1fmullem  25628  i1fadd  25629  itg1addlem2  25631  i1fmulc  25637  itg1mulc  25638  ellimc3  25813  limcmpt2  25818  dvlem  25830  dvidlem  25849  dvcnp  25853  dvcobr  25882  dvcobrOLD  25883  dvrec  25892  dvrecg  25910  dvmptdiv  25911  dvcnvlem  25913  dvexp3  25915  dveflem  25916  dvferm1lem  25921  dvferm2lem  25923  lhop1lem  25951  ftc1lem5  25980  mdegleb  26002  coe1mul3  26037  ply1nz  26060  fta1blem  26109  fta1b  26110  ig1peu  26113  ig1pdvds  26118  plyeq0lem  26148  dgrub  26172  quotval  26233  fta1lem  26248  fta1  26249  elqaalem3  26262  qaa  26264  iaa  26266  aareccl  26267  aannenlem2  26270  abelthlem8  26382  abelth  26384  eff1olem  26490  logrncl  26509  eflog  26518  logeftb  26525  logdmss  26584  dvlog  26593  logbcl  26710  logbid1  26711  logb1  26712  elogb  26713  logbchbase  26714  relogbval  26715  relogbcl  26716  relogbreexp  26718  relogbmul  26720  nnlogbexp  26724  relogbcxp  26728  cxplogb  26729  relogbcxpb  26730  logbf  26732  logblog  26735  2logb9irrALT  26741  sqrt2cxp2logb9e3  26742  angval  26744  dcubic  26789  rlimcnp  26908  efrlim  26912  efrlimOLD  26913  logexprlim  27169  dchrghm  27200  dchrabs  27204  lgsfcl2  27247  lgsval2lem  27251  lgsval3  27259  lgsmod  27267  lgsdirprm  27275  lgsne0  27279  gausslemma2dlem0f  27305  lgsquad2lem2  27329  2lgsoddprm  27360  2sqlem11  27373  2sqblem  27375  dchrvmaeq0  27448  rpvmasum2  27456  dchrisum0re  27457  qrngdiv  27568  addsval  27909  divsval  28132  elnns  28272  1nns  28281  tglngval  28531  tgisline  28607  axlowdimlem9  28930  axlowdimlem12  28933  axlowdimlem13  28934  elntg2  28965  upgrbi  29073  upgr1elem  29092  umgrislfupgrlem  29102  edgupgr  29114  subgruhgredgd  29264  upgrreslem  29284  nbgrel  29320  nbupgr  29324  nbupgrel  29325  nbumgrvtx  29326  nbgrssovtx  29341  nbupgrres  29344  nbusgrvtxm1uvtx  29385  nbupgruvtxres  29387  iscplgredg  29397  cusgredg  29404  cusgrfilem2  29437  usgredgsscusgredg  29440  1loopgrnb0  29483  1egrvtxdg0  29492  uhgrvd00  29515  vtxdginducedm1lem4  29523  eupth2lem3lem3  30209  frcond1  30245  frcond4  30249  2pthfrgr  30263  3cyclfrgrrn1  30264  n4cyclfrgr  30270  frgrwopreglem4a  30289  numclwwlk5  30367  ressupprn  32663  suppss3  32697  xdivval  32889  xrge0tsmsd  33045  pmtrcnel  33061  pmtrcnelor  33063  0nellinds  33334  dvdsruasso  33349  mxidlirredi  33435  extdg1id  33654  irngnzply1  33679  submatminr1  33793  ordtconnlem1  33907  ispisys2  34136  sigapisys  34138  sibfinima  34323  sseqf  34376  signswch  34545  signstfvn  34553  signsvtn0  34554  signstfvneq0  34556  signstfvcl  34557  signstfveq0a  34560  signstfveq0  34561  signsvfn  34566  signsvtp  34567  signsvtn  34568  signsvfpn  34569  signsvfnn  34570  signlem0  34571  bnj158  34712  bnj168  34713  bnj529  34724  bnj906  34913  bnj970  34930  exdifsn  35062  cusgredgex2  35103  subfacp1lem5  35164  cvmsi  35245  cvmsval  35246  cvmsdisj  35250  cvmscld  35253  cvmsss2  35254  satfv1lem  35342  sinccvglem  35652  circum  35654  mpomulnzcnf  36280  unbdqndv2lem2  36491  bj-0int  37082  lindsadd  37600  lindsenlbs  37602  matunitlindflem2  37604  matunitlindf  37605  poimirlem6  37613  poimirlem7  37614  poimirlem8  37615  poimirlem16  37623  poimirlem18  37625  poimirlem19  37626  poimirlem21  37628  poimirlem22  37629  poimirlem24  37631  poimirlem25  37632  poimirlem26  37633  poimirlem27  37634  itg2addnclem2  37659  sdclem1  37730  rrncmslem  37819  rrnequiv  37822  isdrngo2  37945  isdrngo3  37946  eldmxrncnvepres  38389  eldmxrncnvepres2  38390  prtlem100  38845  prter2  38867  prter3  38868  lsatlspsn2  38978  lsateln0  38981  lsatn0  38985  lsatspn0  38986  lsatcmp  38989  lsatelbN  38992  islshpat  39003  lsat0cv  39019  lkrlspeqN  39157  dvheveccl  41099  dihlatat  41324  dochnel  41380  dihjat1  41416  dvh4dimlem  41430  dochsnkr2cl  41461  dochkr1  41465  dochkr1OLDN  41466  lcfl6lem  41485  lcfl9a  41492  lclkrlem2l  41505  lclkrlem2o  41508  lclkrlem2q  41510  lcfrlem9  41537  lcfrlem16  41545  lcfrlem17  41546  lcfrlem27  41556  lcfrlem37  41566  lcfrlem38  41567  lcfrlem40  41569  lcdlkreqN  41609  mapdrvallem2  41632  mapdn0  41656  mapdpglem20  41678  mapdpglem30  41689  mapdindp0  41706  mapdhcl  41714  mapdh6aN  41722  mapdh6dN  41726  mapdh6eN  41727  mapdh6kN  41733  mapdh8  41775  hdmap1l6a  41796  hdmap1l6d  41800  hdmap1l6e  41801  hdmap1l6k  41807  hdmapval3N  41825  hdmap10  41827  hdmap11lem2  41829  hdmapnzcl  41832  hdmaprnlem3eN  41845  hdmaprnlem17N  41850  hdmap14lem4a  41858  hdmap14lem7  41861  hdmap14lem14  41868  hgmaprnlem5N  41887  hdmaplkr  41900  hdmapip0  41902  hgmapvvlem2  41911  hgmapvvlem3  41912  hgmapvv  41913  redvmptabs  42341  readvrec2  42342  readvrec  42343  fiabv  42517  fsuppind  42571  0prjspnlem  42604  pellexlem5  42814  dfac11  43044  dfacbasgrp  43090  dgraalem  43127  dgraaub  43130  aaitgo  43144  proot1ex  43178  deg1mhm  43182  ofdivrec  44308  ofdivcan4  44309  ofdivdiv2  44310  expgrowth  44317  binomcxplemnotnn0  44338  dvdivbd  45914  dvdivcncf  45918  dirkeritg  46093  fourierdlem39  46137  fourierdlem57  46154  fourierdlem58  46155  fourierdlem59  46156  fourierdlem68  46165  fourierdlem76  46173  fourierdlem103  46200  fourierdlem104  46201  fourierdlem111  46208  setsnidel  47371  sprvalpwn0  47477  odz2prm2pw  47557  fmtnoprmfac1  47559  fmtnoprmfac2  47561  sfprmdvdsmersenne  47597  lighneallem2  47600  lighneallem3  47601  lighneal  47605  oddprmALTV  47681  evenprm2  47708  oddprmne2  47709  odd2prm2  47712  even3prm2  47713  isubgruhgr  47861  grimuhgr  47880  2zrngnmrid  48237  lincext1  48436  lindslinindsimp2lem5  48444  rege1logbrege0  48540  fllogbd  48542  relogbmulbexp  48543  relogbdivb  48544  nnpw2blen  48562  blennngt2o2  48574  blennn0e2  48576  dignn0ldlem  48584  line  48714  rrxline  48716  aacllem  49783