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

Theorem eldifsn 4747
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 3920 . 2 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2 elsng 4600 . . . 4 (𝐴𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
32necon3bbid 2981 . . 3 (𝐴𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴𝐶))
43pm5.32i 575 . 2 ((𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
51, 4bitri 274 1 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 396  wcel 2106  wne 2943  cdif 3907  {csn 4586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-v 3447  df-dif 3913  df-sn 4587
This theorem is referenced by:  elpwdifsn  4749  eldifsni  4750  rexdifsn  4754  raldifsni  4755  eldifvsn  4757  difsn  4758  prproe  4863  sossfld  6138  tpres  7149  onmindif2  7741  xpord3pred  8083  xpord3inddlem  8085  mptsuppd  8117  suppssr  8126  suppssov1  8128  suppsssn  8131  suppssfv  8132  dif1o  8445  difsnen  8996  limenpsi  9095  frfi  9231  fofinf1o  9270  en2eleq  9943  en2other2  9944  dfac8clem  9967  acni2  9981  acndom  9986  acnnum  9987  dfac9  10071  dfacacn  10076  kmlem3  10087  kmlem4  10088  fin23lem21  10274  canthp1lem2  10588  elni  10811  mulnzcnopr  11800  divval  11814  elnnne0  12426  elq  12874  rpcndif0  12933  modfzo0difsn  13847  modsumfzodifsn  13848  expcl2lem  13978  expclzlem  13988  hashdifpr  14314  hashgt23el  14323  prprrab  14371  hashle2prv  14376  reccn2  15478  rlimdiv  15529  eff2  15980  tanval  16009  rpnnen2lem9  16103  fzo0dvdseq  16204  oddprmgt2  16574  oddprmdvds  16774  4sqlem19  16834  prmlem0  16977  prmlem1a  16978  setsnid  17080  setsnidOLD  17081  grpinvnzcl  18817  symgextf  19197  f1omvdmvd  19223  pmtrprfv  19233  odcau  19384  efgsf  19509  efgsrel  19514  efgs1  19515  efgs1b  19516  efgsp1  19517  efgsres  19518  efgredlema  19520  efgredlemd  19524  efgrelexlemb  19530  gsumpt  19737  dmdprdd  19776  dprdcntz  19785  dprdfeq0  19799  dprd2da  19819  drngunit  20188  isdrng2  20196  drngid2  20202  isdrngd  20212  issubdrg  20245  sdrgacs  20266  cntzsdrg  20267  abvtriv  20298  islss  20393  lssneln0  20411  lssssr  20412  lbsind  20539  lbspss  20541  lspabs3  20580  lspsneq  20581  lspfixed  20587  lspexch  20588  islbs2  20613  isdomn2  20767  domnrrg  20768  cnflddiv  20825  cnfldinv  20826  xrs1mnd  20833  xrs10  20834  xrge0subm  20836  cnsubdrglem  20846  cnmgpid  20857  cnmsubglem  20858  gzrngunit  20861  zringunit  20885  zringndrg  20887  domnchr  20933  cnmsgngrp  20981  psgninv  20984  psgndiflemB  21002  lindfind  21220  lindsind  21221  lindff1  21224  lindfrn  21225  mvrcl  21419  coe1tmmul2  21645  mdetunilem9  21967  maducoeval2  21987  gsummatr01lem4  22005  ist1-2  22696  cmpfi  22757  2ndcdisj  22805  2ndcsep  22808  locfincmp  22875  alexsublem  23393  cldsubg  23460  imasdsf1olem  23724  prdsxmslem2  23883  reperflem  24179  xrge0gsumle  24194  xrge0tsms  24195  divcn  24229  evth  24320  cvsdiv  24493  cvsdivcl  24494  cphreccllem  24540  bcthlem5  24690  itg11  25053  i1fmullem  25056  i1fadd  25057  itg1addlem2  25059  i1fmulc  25066  itg1mulc  25067  ellimc3  25241  limcmpt2  25246  dvlem  25258  dvidlem  25277  dvcnp  25281  dvcobr  25308  dvrec  25317  dvrecg  25335  dvmptdiv  25336  dvcnvlem  25338  dvexp3  25340  dveflem  25341  dvferm1lem  25346  dvferm2lem  25348  lhop1lem  25375  ftc1lem5  25402  mdegleb  25427  coe1mul3  25462  ply1nz  25484  fta1blem  25531  fta1b  25532  ig1peu  25534  ig1pdvds  25539  plyeq0lem  25569  dgrub  25593  quotval  25650  fta1lem  25665  fta1  25666  elqaalem3  25679  qaa  25681  iaa  25683  aareccl  25684  aannenlem2  25687  abelthlem8  25796  abelth  25798  eff1olem  25902  logrncl  25921  eflog  25930  logeftb  25937  logdmss  25995  dvlog  26004  logbcl  26115  logbid1  26116  logb1  26117  elogb  26118  logbchbase  26119  relogbval  26120  relogbcl  26121  relogbreexp  26123  relogbmul  26125  nnlogbexp  26129  relogbcxp  26133  cxplogb  26134  relogbcxpb  26135  logbf  26137  logblog  26140  2logb9irrALT  26146  sqrt2cxp2logb9e3  26147  angval  26149  dcubic  26194  rlimcnp  26313  efrlim  26317  logexprlim  26571  dchrghm  26602  dchrabs  26606  lgsfcl2  26649  lgsval2lem  26653  lgsval3  26661  lgsmod  26669  lgsdirprm  26677  lgsne0  26681  gausslemma2dlem0f  26707  lgsquad2lem2  26731  2lgsoddprm  26762  2sqlem11  26775  2sqblem  26777  dchrvmaeq0  26850  rpvmasum2  26858  dchrisum0re  26859  qrngdiv  26970  addsval  27272  tglngval  27440  tgisline  27516  axlowdimlem9  27846  axlowdimlem12  27849  axlowdimlem13  27850  elntg2  27881  upgrbi  27991  upgr1elem  28010  umgrislfupgrlem  28020  edgupgr  28032  subgruhgredgd  28179  upgrreslem  28199  nbgrel  28235  nbupgr  28239  nbupgrel  28240  nbumgrvtx  28241  nbgrssovtx  28256  nbupgrres  28259  nbusgrvtxm1uvtx  28300  nbupgruvtxres  28302  iscplgredg  28312  cusgredg  28319  cusgrfilem2  28351  usgredgsscusgredg  28354  1loopgrnb0  28397  1egrvtxdg0  28406  uhgrvd00  28429  vtxdginducedm1lem4  28437  eupth2lem3lem3  29121  frcond1  29157  frcond4  29161  2pthfrgr  29175  3cyclfrgrrn1  29176  n4cyclfrgr  29182  frgrwopreglem4a  29201  numclwwlk5  29279  ressupprn  31550  suppss3  31585  xdivval  31719  xrge0tsmsd  31843  pmtrcnel  31884  pmtrcnelor  31886  0nellinds  32103  extdg1id  32292  irngnzply1  32305  submatminr1  32331  ordtconnlem1  32445  ispisys2  32692  sigapisys  32694  sibfinima  32879  sseqf  32932  signswch  33113  signstfvn  33121  signsvtn0  33122  signstfvneq0  33124  signstfvcl  33125  signstfveq0a  33128  signstfveq0  33129  signsvfn  33134  signsvtp  33135  signsvtn  33136  signsvfpn  33137  signsvfnn  33138  signlem0  33139  bnj158  33281  bnj168  33282  bnj529  33293  bnj906  33482  bnj970  33499  exdifsn  33625  cusgredgex2  33656  subfacp1lem5  33718  cvmsi  33799  cvmsval  33800  cvmsdisj  33804  cvmscld  33807  cvmsss2  33808  satfv1lem  33896  sinccvglem  34200  circum  34202  unbdqndv2lem2  34963  bj-0int  35562  lindsadd  36061  lindsenlbs  36063  matunitlindflem2  36065  matunitlindf  36066  poimirlem6  36074  poimirlem7  36075  poimirlem8  36076  poimirlem16  36084  poimirlem18  36086  poimirlem19  36087  poimirlem21  36089  poimirlem22  36090  poimirlem24  36092  poimirlem25  36093  poimirlem26  36094  poimirlem27  36095  itg2addnclem2  36120  sdclem1  36192  rrncmslem  36281  rrnequiv  36284  isdrngo2  36407  isdrngo3  36408  prtlem100  37311  prter2  37333  prter3  37334  lsatlspsn2  37444  lsateln0  37447  lsatn0  37451  lsatspn0  37452  lsatcmp  37455  lsatelbN  37458  islshpat  37469  lsat0cv  37485  lkrlspeqN  37623  dvheveccl  39565  dihlatat  39790  dochnel  39846  dihjat1  39882  dvh4dimlem  39896  dochsnkr2cl  39927  dochkr1  39931  dochkr1OLDN  39932  lcfl6lem  39951  lcfl9a  39958  lclkrlem2l  39971  lclkrlem2o  39974  lclkrlem2q  39976  lcfrlem9  40003  lcfrlem16  40011  lcfrlem17  40012  lcfrlem27  40022  lcfrlem37  40032  lcfrlem38  40033  lcfrlem40  40035  lcdlkreqN  40075  mapdrvallem2  40098  mapdn0  40122  mapdpglem20  40144  mapdpglem30  40155  mapdindp0  40172  mapdhcl  40180  mapdh6aN  40188  mapdh6dN  40192  mapdh6eN  40193  mapdh6kN  40199  mapdh8  40241  hdmap1l6a  40262  hdmap1l6d  40266  hdmap1l6e  40267  hdmap1l6k  40273  hdmapval3N  40291  hdmap10  40293  hdmap11lem2  40295  hdmapnzcl  40298  hdmaprnlem3eN  40311  hdmaprnlem17N  40316  hdmap14lem4a  40324  hdmap14lem7  40327  hdmap14lem14  40334  hgmaprnlem5N  40353  hdmaplkr  40366  hdmapip0  40368  hgmapvvlem2  40377  hgmapvvlem3  40378  hgmapvv  40379  fsuppind  40742  0prjspnlem  40938  pellexlem5  41133  dfac11  41366  dfacbasgrp  41412  dgraalem  41449  dgraaub  41452  aaitgo  41466  proot1ex  41505  isdomn3  41508  deg1mhm  41511  ofdivrec  42587  ofdivcan4  42588  ofdivdiv2  42589  expgrowth  42596  binomcxplemnotnn0  42617  dvdivbd  44135  dvdivcncf  44139  dirkeritg  44314  fourierdlem39  44358  fourierdlem57  44375  fourierdlem58  44376  fourierdlem59  44377  fourierdlem68  44386  fourierdlem76  44394  fourierdlem103  44421  fourierdlem104  44422  fourierdlem111  44429  setsnidel  45540  sprvalpwn0  45646  odz2prm2pw  45726  fmtnoprmfac1  45728  fmtnoprmfac2  45730  sfprmdvdsmersenne  45766  lighneallem2  45769  lighneallem3  45770  lighneal  45774  oddprmALTV  45850  evenprm2  45877  oddprmne2  45878  odd2prm2  45881  even3prm2  45882  2zrngnmrid  46219  lincext1  46506  lindslinindsimp2lem5  46514  rege1logbrege0  46615  fllogbd  46617  relogbmulbexp  46618  relogbdivb  46619  nnpw2blen  46637  blennngt2o2  46649  blennn0e2  46651  dignn0ldlem  46659  line  46789  rrxline  46791  aacllem  47219
  Copyright terms: Public domain W3C validator