MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eldifsn Structured version   Visualization version   GIF version

Theorem eldifsn 4350
Description: Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
Assertion
Ref Expression
eldifsn (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))

Proof of Theorem eldifsn
StepHypRef Expression
1 eldif 3617 . 2 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2 elsng 4224 . . . 4 (𝐴𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
32necon3bbid 2860 . . 3 (𝐴𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴𝐶))
43pm5.32i 670 . 2 ((𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
51, 4bitri 264 1 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wa 383  wcel 2030  wne 2823  cdif 3604  {csn 4210
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-v 3233  df-dif 3610  df-sn 4211
This theorem is referenced by:  ssdifsn  4351  elpwdifsn  4352  eldifsni  4353  rexdifsn  4356  raldifsni  4357  eldifvsn  4359  difsn  4360  prproe  4466  sossfld  5615  tpres  6507  mpt2difsnif  6795  onmindif2  7054  mptsuppd  7363  suppssr  7371  suppssov1  7372  suppsssn  7375  suppssfv  7376  dif1o  7625  difsnen  8083  limenpsi  8176  frfi  8246  fofinf1o  8282  wemapso2lem  8498  en2eleq  8869  en2other2  8870  dfac8clem  8893  acni2  8907  acndom  8912  acnnum  8913  dfac9  8996  dfacacn  9001  kmlem3  9012  kmlem4  9013  fin23lem21  9199  canthp1lem2  9513  elni  9736  mulnzcnopr  10711  divval  10725  elnnne0  11344  elq  11828  rpcndif0  11889  modfzo0difsn  12782  modsumfzodifsn  12783  expcl2lem  12912  expclzlem  12924  hashdifpr  13241  prprrab  13293  hashle2prv  13298  reccn2  14371  rlimdiv  14420  eff2  14873  tanval  14902  rpnnen2lem9  14995  fzo0dvdseq  15092  oddprmgt2  15458  prmn2uzge3OLD  15460  oddprmdvds  15654  4sqlem19  15714  prmlem0  15859  prmlem1a  15860  setsnid  15962  grpinvnzcl  17534  symgextf  17883  symgextfv  17884  f1omvdmvd  17909  pmtrprfv  17919  odcau  18065  efgsf  18188  efgsrel  18193  efgs1  18194  efgs1b  18195  efgsp1  18196  efgsres  18197  efgredlema  18199  efgredlemd  18203  efgrelexlemb  18209  gsumpt  18407  dmdprdd  18444  dprdcntz  18453  dprdfeq0  18467  dprd2da  18487  drngunit  18800  isdrng2  18805  drngid2  18811  isdrngd  18820  issubdrg  18853  abvtriv  18889  islss  18983  lssneln0  19000  lssssr  19001  lbsind  19128  lbspss  19130  lspabs3  19169  lspsneq  19170  lspfixed  19176  lspexch  19177  islbs2  19202  isdomn2  19347  domnrrg  19348  mvrcl  19497  coe1tmmul2  19694  cnflddiv  19824  cnfldinv  19825  xrs1mnd  19832  xrs10  19833  xrge0subm  19835  cnsubdrglem  19845  cnmgpid  19856  cnmsubglem  19857  gzrngunit  19860  zringunit  19884  zringndrg  19886  domnchr  19928  cnmsgngrp  19973  psgninv  19976  psgndiflemB  19994  lindfind  20203  lindsind  20204  lindff1  20207  lindfrn  20208  mdetunilem9  20474  maducoeval2  20494  gsummatr01lem4  20512  ist1-2  21199  cmpfi  21259  2ndcdisj  21307  2ndcsep  21310  locfincmp  21377  alexsublem  21895  cldsubg  21961  imasdsf1olem  22225  prdsxmslem2  22381  reperflem  22668  xrge0gsumle  22683  xrge0tsms  22684  divcn  22718  evth  22805  cvsdiv  22978  cvsdivcl  22979  cphreccllem  23024  bcthlem5  23171  itg11  23503  i1fmullem  23506  i1fadd  23507  itg1addlem2  23509  i1fmulc  23515  itg1mulc  23516  ellimc3  23688  limcmpt2  23693  dvlem  23705  dvidlem  23724  dvcnp  23727  dvcobr  23754  dvrec  23763  dvrecg  23781  dvmptdiv  23782  dvcnvlem  23784  dvexp3  23786  dveflem  23787  dvferm1lem  23792  dvferm2lem  23794  lhop1lem  23821  ftc1lem5  23848  mdegleb  23869  coe1mul3  23904  ply1nz  23926  fta1blem  23973  fta1b  23974  ig1peu  23976  ig1pdvds  23981  plyeq0lem  24011  dgrub  24035  quotval  24092  fta1lem  24107  fta1  24108  elqaalem3  24121  qaa  24123  iaa  24125  aareccl  24126  aannenlem2  24129  abelthlem8  24238  abelth  24240  reefgim  24249  eff1olem  24339  logrncl  24359  eflog  24368  logeftb  24375  logdmss  24433  dvlog  24442  logbcl  24550  logbid1  24551  logb1  24552  elogb  24553  logbchbase  24554  relogbval  24555  relogbcl  24556  relogbreexp  24558  relogbmul  24560  nnlogbexp  24564  relogbcxp  24568  cxplogb  24569  relogbcxpb  24570  logbf  24572  logblog  24575  angval  24576  dcubic  24618  rlimcnp  24737  efrlim  24741  logexprlim  24995  dchrghm  25026  dchrabs  25030  lgsfcl2  25073  lgsval2lem  25077  lgsval3  25085  lgsmod  25093  lgsdirprm  25101  lgsne0  25105  gausslemma2dlem0f  25131  lgsquad2lem2  25155  2lgsoddprm  25186  2sqlem11  25199  2sqblem  25201  dchrvmaeq0  25238  rpvmasum2  25246  dchrisum0re  25247  qrngdiv  25358  tglngval  25491  tgisline  25567  axlowdimlem9  25875  axlowdimlem12  25878  axlowdimlem13  25879  upgrbi  26033  upgr1elem  26052  umgrislfupgrlem  26062  edgupgr  26074  subgruhgredgd  26221  upgrreslem  26241  nbgrel  26278  nbgrelOLD  26279  nbupgr  26285  nbupgrel  26286  nbumgrvtx  26287  nbgrssovtx  26302  nbgrssovtxOLD  26305  nbupgrres  26310  nbusgrvtxm1uvtx  26356  nbupgruvtxres  26358  iscplgredg  26369  cusgredg  26376  cusgrfilem2  26408  usgredgsscusgredg  26411  1loopgrnb0  26454  1egrvtxdg0  26463  uhgrvd00  26486  vtxdginducedm1lem4  26494  eupth2lem3lem3  27208  frcond1  27246  frcond4  27250  2pthfrgr  27264  3cyclfrgrrn1  27265  n4cyclfrgr  27271  frgrwopreglem4a  27290  numclwwlk5  27375  suppss3  29630  xdivval  29755  xrge0tsmsd  29913  submatminr1  30004  ordtconnlem1  30098  ispisys2  30344  sigapisys  30346  sibfinima  30529  sseqf  30582  signswch  30766  signstfvn  30774  signsvtn0  30775  signstfvcl  30778  signstfveq0a  30781  signstfveq0  30782  signsvfn  30787  signsvtp  30788  signsvtn  30789  signsvfpn  30790  signsvfnn  30791  signlem0  30792  bnj158  30923  bnj168  30924  bnj529  30937  bnj906  31126  bnj970  31143  subfacp1lem5  31292  cvmsi  31373  cvmsval  31374  cvmsdisj  31378  cvmscld  31381  cvmsss2  31382  sinccvglem  31692  circum  31694  unbdqndv2lem2  32626  bj-0int  33180  lindsenlbs  33534  matunitlindflem2  33536  matunitlindf  33537  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem16  33555  poimirlem18  33557  poimirlem19  33558  poimirlem21  33560  poimirlem22  33561  poimirlem24  33563  poimirlem25  33564  poimirlem26  33565  poimirlem27  33566  itg2addnclem2  33592  sdclem1  33669  rrncmslem  33761  rrnequiv  33764  isdrngo2  33887  isdrngo3  33888  prtlem100  34463  prter2  34485  prter3  34486  lsatlspsn2  34597  lsateln0  34600  lsatn0  34604  lsatspn0  34605  lsatcmp  34608  lsatelbN  34611  islshpat  34622  lsat0cv  34638  lkrlspeqN  34776  dvheveccl  36718  dihlatat  36943  dochnel  36999  dihjat1  37035  dvh4dimlem  37049  dochsnkr2cl  37080  dochkr1  37084  dochkr1OLDN  37085  lcfl6lem  37104  lcfl9a  37111  lclkrlem2l  37124  lclkrlem2o  37127  lclkrlem2q  37129  lcfrlem9  37156  lcfrlem16  37164  lcfrlem17  37165  lcfrlem27  37175  lcfrlem37  37185  lcfrlem38  37186  lcfrlem40  37188  lcdlkreqN  37228  mapdrvallem2  37251  mapdn0  37275  mapdpglem20  37297  mapdpglem30  37308  mapdindp0  37325  mapdhcl  37333  mapdh6aN  37341  mapdh6dN  37345  mapdh6eN  37346  mapdh6kN  37352  mapdh8  37395  hdmap1l6a  37416  hdmap1l6d  37420  hdmap1l6e  37421  hdmap1l6k  37427  hdmapval3N  37447  hdmap10  37449  hdmap11lem2  37451  hdmapnzcl  37454  hdmaprnlem3eN  37467  hdmaprnlem17N  37472  hdmap14lem4a  37480  hdmap14lem7  37483  hdmap14lem14  37490  hgmaprnlem5N  37509  hdmaplkr  37522  hdmapip0  37524  hgmapvvlem2  37533  hgmapvvlem3  37534  hgmapvv  37535  pellexlem5  37714  dfac11  37949  dfacbasgrp  37995  dgraalem  38032  dgraaub  38035  aaitgo  38049  sdrgacs  38088  cntzsdrg  38089  proot1ex  38096  isdomn3  38099  deg1mhm  38102  ofdivrec  38842  ofdivcan4  38843  ofdivdiv2  38844  expgrowth  38851  binomcxplemnotnn0  38872  dvdivbd  40456  dvdivcncf  40460  dirkeritg  40637  fourierdlem39  40681  fourierdlem57  40698  fourierdlem58  40699  fourierdlem59  40700  fourierdlem68  40709  fourierdlem76  40717  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  setsnidel  41672  odz2prm2pw  41800  fmtnoprmfac1  41802  fmtnoprmfac2  41804  sfprmdvdsmersenne  41845  lighneallem2  41848  lighneallem3  41849  lighneal  41853  oddprmALTV  41923  evenprm2  41948  oddprmne2  41949  odd2prm2  41952  even3prm2  41953  sprvalpwn0  42058  2zrngnmrid  42275  fdmdifeqresdif  42445  lincext1  42568  lindslinindsimp2lem5  42576  rege1logbrege0  42677  fllogbd  42679  relogbmulbexp  42680  relogbdivb  42681  nnpw2blen  42699  blennngt2o2  42711  blennn0e2  42713  dignn0ldlem  42721  aacllem  42875
  Copyright terms: Public domain W3C validator