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

Theorem eldifsn 4260
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 3550 . 2 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2 elsng 4139 . . . 4 (𝐴𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
32necon3bbid 2819 . . 3 (𝐴𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴𝐶))
43pm5.32i 667 . 2 ((𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
51, 4bitri 263 1 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 195  wa 383  wcel 1977  wne 2780  cdif 3537  {csn 4125
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-v 3175  df-dif 3543  df-sn 4126
This theorem is referenced by:  eldifsni  4261  rexdifsn  4264  raldifsni  4265  eldifvsn  4267  difsn  4269  sossfld  5499  tpres  6371  mpt2difsnif  6651  onmindif2  6904  mptsuppd  7205  suppssr  7213  suppssov1  7214  suppsssn  7217  suppssfv  7218  dif1o  7467  difsnen  7927  limenpsi  8020  frfi  8090  fofinf1o  8126  wemapso2lem  8340  en2eleq  8714  en2other2  8715  dfac8clem  8738  acni2  8752  acndom  8757  acnnum  8758  dfac9  8841  dfacacn  8846  kmlem3  8857  kmlem4  8858  fin23lem21  9044  canthp1lem2  9354  elni  9577  mulnzcnopr  10552  divval  10566  elnnne0  11183  elq  11666  rpcndif0  11727  modfzo0difsn  12604  modsumfzodifsn  12605  expcl2lem  12734  expclzlem  12746  hashdifpr  13064  prprrab  13112  reccn2  14175  rlimdiv  14224  eff2  14668  tanval  14697  rpnnen2lem9  14790  fzo0dvdseq  14883  oddprmgt2  15249  prmn2uzge3OLD  15251  oddprmdvds  15445  4sqlem19  15505  prmlem0  15650  prmlem1a  15651  setsnid  15743  grpinvnzcl  17310  symgextf  17660  symgextfv  17661  f1omvdmvd  17686  pmtrprfv  17696  odcau  17842  efgsf  17965  efgsrel  17970  efgs1  17971  efgs1b  17972  efgsp1  17973  efgsres  17974  efgredlema  17976  efgredlemd  17980  efgrelexlemb  17986  gsumpt  18184  dmdprdd  18221  dprdcntz  18230  dprdfeq0  18244  dprd2da  18264  drngunit  18575  isdrng2  18580  drngid2  18586  isdrngd  18595  issubdrg  18628  abvtriv  18664  islss  18756  lssneln0  18773  lssssr  18774  lbsind  18901  lbspss  18903  lspabs3  18942  lspsneq  18943  lspfixed  18949  lspexch  18950  islbs2  18975  isdomn2  19120  domnrrg  19121  mvrcl  19270  coe1tmmul2  19467  cnflddiv  19595  cnfldinv  19596  xrs1mnd  19603  xrs10  19604  xrge0subm  19606  cnsubdrglem  19616  cnmgpid  19627  cnmsubglem  19628  gzrngunit  19631  zringunit  19655  zringndrg  19657  domnchr  19699  cnmsgngrp  19744  psgninv  19747  psgndiflemB  19765  lindfind  19974  lindsind  19975  lindff1  19978  lindfrn  19979  mdetunilem9  20245  maducoeval2  20265  gsummatr01lem4  20283  ist1-2  20961  cmpfi  21021  2ndcdisj  21069  2ndcsep  21072  locfincmp  21139  alexsublem  21658  cldsubg  21724  imasdsf1olem  21988  prdsxmslem2  22144  reperflem  22429  xrge0gsumle  22444  xrge0tsms  22445  divcn  22479  evth  22566  cvsdiv  22740  cvsdivcl  22741  cphreccllem  22786  bcthlem5  22933  itg11  23264  i1fmullem  23267  i1fadd  23268  itg1addlem2  23270  i1fmulc  23276  itg1mulc  23277  ellimc3  23449  limcmpt2  23454  dvlem  23466  dvidlem  23485  dvcnp  23488  dvcobr  23515  dvrec  23524  dvcnvlem  23543  dvexp3  23545  dveflem  23546  dvferm1lem  23551  dvferm2lem  23553  lhop1lem  23580  ftc1lem5  23607  mdegleb  23628  coe1mul3  23663  ply1nz  23685  fta1blem  23732  fta1b  23733  ig1peu  23735  ig1pdvds  23740  plyeq0lem  23770  dgrub  23794  quotval  23851  fta1lem  23866  fta1  23867  elqaalem3  23880  qaa  23882  iaa  23884  aareccl  23885  aannenlem2  23888  abelthlem8  23997  abelth  23999  reefgim  24008  eff1olem  24098  logrncl  24118  eflog  24127  logeftb  24134  logdmss  24188  dvlog  24197  logbcl  24305  logbid1  24306  logb1  24307  elogb  24308  logbchbase  24309  relogbval  24310  relogbcl  24311  relogbreexp  24313  relogbmul  24315  nnlogbexp  24319  relogbcxp  24323  cxplogb  24324  relogbcxpb  24325  logbf  24327  logblog  24330  angval  24331  dcubic  24373  rlimcnp  24492  efrlim  24496  logexprlim  24750  dchrghm  24781  dchrabs  24785  lgsfcl2  24828  lgsval2lem  24832  lgsval3  24840  lgsmod  24848  lgsdirprm  24856  lgsne0  24860  gausslemma2dlem0f  24886  lgsquad2lem2  24910  2lgsoddprm  24941  2sqlem11  24954  2sqblem  24956  dchrvmaeq0  24993  rpvmasum2  25001  dchrisum0re  25002  qrngdiv  25113  tglngval  25246  tgisline  25322  axlowdimlem9  25630  axlowdimlem12  25633  axlowdimlem13  25634  upgrbi  25760  upgr1elem  25778  umgrislfupgrlem  25788  edgupgr  25808  upgredg  25811  umgra1  25855  uslgra1  25901  cusgrarn  25988  cusgrafilem2  26008  sizeusglecusglem1  26012  nbhashuvtx  26443  umgrabi  26510  2pthfrgra  26538  3cyclfrgrarn1  26539  n4cyclfrgra  26545  numclwwlk5  26639  suppss3  28890  xdivval  28958  xrge0tsmsd  29116  submatminr1  29204  ordtconlem1  29298  ispisys2  29543  sigapisys  29545  sibfinima  29728  sseqf  29781  signswch  29964  signstfvn  29972  signsvtn0  29973  signstfvcl  29976  signstfveq0a  29979  signstfveq0  29980  signsvfn  29985  signsvtp  29986  signsvtn  29987  signsvfpn  29988  signsvfnn  29989  signlem0  29990  bnj158  30051  bnj168  30052  bnj529  30065  bnj906  30254  bnj970  30271  subfacp1lem5  30420  cvmsi  30501  cvmsval  30502  cvmsdisj  30506  cvmscld  30509  cvmsss2  30510  sinccvglem  30820  circum  30822  unbdqndv2lem2  31671  lindsenlbs  32574  matunitlindflem2  32576  matunitlindf  32577  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem16  32595  poimirlem18  32597  poimirlem19  32598  poimirlem21  32600  poimirlem22  32601  poimirlem24  32603  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  itg2addnclem2  32632  sdclem1  32709  rrncmslem  32801  rrnequiv  32804  isdrngo2  32927  isdrngo3  32928  prtlem100  33161  prter2  33184  prter3  33185  lsatlspsn2  33297  lsateln0  33300  lsatn0  33304  lsatspn0  33305  lsatcmp  33308  lsatelbN  33311  islshpat  33322  lsat0cv  33338  lkrlspeqN  33476  dvheveccl  35419  dihlatat  35644  dochnel  35700  dihjat1  35736  dvh4dimlem  35750  dochsnkr2cl  35781  dochkr1  35785  dochkr1OLDN  35786  lcfl6lem  35805  lcfl9a  35812  lclkrlem2l  35825  lclkrlem2o  35828  lclkrlem2q  35830  lcfrlem9  35857  lcfrlem16  35865  lcfrlem17  35866  lcfrlem27  35876  lcfrlem37  35886  lcfrlem38  35887  lcfrlem40  35889  lcdlkreqN  35929  mapdrvallem2  35952  mapdn0  35976  mapdpglem20  35998  mapdpglem30  36009  mapdindp0  36026  mapdhcl  36034  mapdh6aN  36042  mapdh6dN  36046  mapdh6eN  36047  mapdh6kN  36053  mapdh8  36096  hdmap1l6a  36117  hdmap1l6d  36121  hdmap1l6e  36122  hdmap1l6k  36128  hdmapval3N  36148  hdmap10  36150  hdmap11lem2  36152  hdmapnzcl  36155  hdmaprnlem3eN  36168  hdmaprnlem17N  36173  hdmap14lem4a  36181  hdmap14lem7  36184  hdmap14lem14  36191  hgmaprnlem5N  36210  hdmaplkr  36223  hdmapip0  36225  hgmapvvlem2  36234  hgmapvvlem3  36235  hgmapvv  36236  pellexlem5  36415  dfac11  36650  dfacbasgrp  36697  dgraalem  36734  dgraaub  36737  aaitgo  36751  sdrgacs  36790  cntzsdrg  36791  proot1ex  36798  isdomn3  36801  deg1mhm  36804  ofdivrec  37547  ofdivcan4  37548  ofdivdiv2  37549  expgrowth  37556  binomcxplemnotnn0  37577  dvrecg  38800  dvmptdiv  38807  dvdivbd  38813  dvdivcncf  38817  dirkeritg  38995  fourierdlem39  39039  fourierdlem57  39056  fourierdlem58  39057  fourierdlem59  39058  fourierdlem68  39067  fourierdlem76  39075  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  odz2prm2pw  40013  fmtnoprmfac1  40015  fmtnoprmfac2  40017  sfprmdvdsmersenne  40058  lighneallem2  40061  lighneallem3  40062  lighneal  40066  oddprmALTV  40136  evenprm2  40161  oddprmne2  40162  elpwdifsn  40312  subgruhgredgd  40508  nbgrel  40564  nbupgr  40566  nbupgrel  40567  nbumgrvtx  40568  nbgrssovtx  40586  nbupgrres  40592  nbusgrvtxm1uvtx  40632  nbupgruvtxres  40634  iscplgredg  40639  cusgredg  40646  cusgrexi  40662  cusgrfilem2  40672  usgredgsscusgredg  40675  1loopgrnb0  40717  1egrvtxdg0  40727  uhgrvd00  40750  eupth2lem3lem3  41398  frcond1  41438  2pthfrgr  41454  3cyclfrgrrn1  41455  n4cyclfrgr  41461  av-numclwwlk5  41542  2zrngnmrid  41740  fdmdifeqresdif  41913  lincext1  42037  lindslinindsimp2lem5  42045  rege1logbrege0  42150  fllogbd  42152  relogbmulbexp  42153  relogbdivb  42154  nnpw2blen  42172  blennngt2o2  42184  blennn0e2  42186  dignn0ldlem  42194  ssdifsn  42228  aacllem  42356
  Copyright terms: Public domain W3C validator