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

Theorem eldifsn 4256
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 3546 . 2 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2 elsng 4135 . . . 4 (𝐴𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
32necon3bbid 2815 . . 3 (𝐴𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴𝐶))
43pm5.32i 666 . 2 ((𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
51, 4bitri 262 1 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194  wa 382  wcel 1976  wne 2776  cdif 3533  {csn 4121
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-v 3171  df-dif 3539  df-sn 4122
This theorem is referenced by:  eldifsni  4257  rexdifsn  4260  raldifsni  4261  eldifvsn  4263  difsn  4265  sossfld  5482  tpres  6346  mpt2difsnif  6626  onmindif2  6878  mptsuppd  7179  suppssr  7187  suppssov1  7188  suppsssn  7191  suppssfv  7192  dif1o  7441  difsnen  7901  limenpsi  7994  frfi  8064  fofinf1o  8100  wemapso2lem  8314  en2eleq  8688  en2other2  8689  dfac8clem  8712  acni2  8726  acndom  8731  acnnum  8732  dfac9  8815  dfacacn  8820  kmlem3  8831  kmlem4  8832  fin23lem21  9018  canthp1lem2  9328  elni  9551  mulnzcnopr  10519  divval  10533  elnnne0  11150  elq  11619  rpcndif0  11680  modfzo0difsn  12556  modsumfzodifsn  12557  expcl2lem  12686  expclzlem  12698  hashdifpr  13013  reccn2  14118  rlimdiv  14167  eff2  14611  tanval  14640  rpnnen2lem9  14733  fzo0dvdseq  14826  oddprmgt2  15192  prmn2uzge3OLD  15194  oddprmdvds  15388  4sqlem19  15448  prmlem0  15593  prmlem1a  15594  setsnid  15686  grpinvnzcl  17253  symgextf  17603  symgextfv  17604  f1omvdmvd  17629  pmtrprfv  17639  odcau  17785  efgsf  17908  efgsrel  17913  efgs1  17914  efgs1b  17915  efgsp1  17916  efgsres  17917  efgredlema  17919  efgredlemd  17923  efgrelexlemb  17929  gsumpt  18127  dmdprdd  18164  dprdcntz  18173  dprdfeq0  18187  dprd2da  18207  drngunit  18518  isdrng2  18523  drngid2  18529  isdrngd  18538  issubdrg  18571  abvtriv  18607  islss  18699  lssneln0  18716  lssssr  18717  lbsind  18844  lbspss  18846  lspabs3  18885  lspsneq  18886  lspfixed  18892  lspexch  18893  islbs2  18918  isdomn2  19063  domnrrg  19064  mvrcl  19213  coe1tmmul2  19410  cnflddiv  19538  cnfldinv  19539  xrs1mnd  19546  xrs10  19547  xrge0subm  19549  cnsubdrglem  19559  cnmgpid  19570  cnmsubglem  19571  gzrngunit  19574  zringunit  19600  domnchr  19641  cnmsgngrp  19686  psgninv  19689  psgndiflemB  19707  lindfind  19913  lindsind  19914  lindff1  19917  lindfrn  19918  mdetunilem9  20184  maducoeval2  20204  gsummatr01lem4  20222  ist1-2  20900  cmpfi  20960  2ndcdisj  21008  2ndcsep  21011  locfincmp  21078  alexsublem  21597  cldsubg  21663  imasdsf1olem  21926  prdsxmslem2  22082  reperflem  22358  xrge0gsumle  22373  xrge0tsms  22374  divcn  22407  evth  22494  cvsdiv  22666  cvsdivcl  22667  cphreccllem  22707  bcthlem5  22847  itg11  23178  i1fmullem  23181  i1fadd  23182  itg1addlem2  23184  i1fmulc  23190  itg1mulc  23191  ellimc3  23363  limcmpt2  23368  dvlem  23380  dvidlem  23399  dvcnp  23402  dvcobr  23429  dvrec  23438  dvcnvlem  23457  dvexp3  23459  dveflem  23460  dvferm1lem  23465  dvferm2lem  23467  lhop1lem  23494  ftc1lem5  23521  mdegleb  23542  coe1mul3  23577  ply1nz  23599  fta1blem  23646  fta1b  23647  ig1peu  23649  ig1pdvds  23654  plyeq0lem  23684  dgrub  23708  quotval  23765  fta1lem  23780  fta1  23781  elqaalem3  23794  qaa  23796  iaa  23798  aareccl  23799  aannenlem2  23802  abelthlem8  23911  abelth  23913  reefgim  23922  eff1olem  24012  logrncl  24032  eflog  24041  logeftb  24048  logdmss  24102  dvlog  24111  logbcl  24219  logbid1  24220  logb1  24221  elogb  24222  logbchbase  24223  relogbval  24224  relogbcl  24225  relogbreexp  24227  relogbmul  24229  nnlogbexp  24233  relogbcxp  24237  cxplogb  24238  relogbcxpb  24239  logbf  24241  logblog  24244  angval  24245  dcubic  24287  rlimcnp  24406  efrlim  24410  logexprlim  24664  dchrghm  24695  dchrabs  24699  lgsfcl2  24742  lgsval2lem  24746  lgsval3  24754  lgsmod  24762  lgsdirprm  24770  lgsne0  24774  gausslemma2dlem0f  24800  lgsquad2lem2  24824  2lgsoddprm  24855  2sqlem11  24868  2sqblem  24870  dchrvmaeq0  24907  rpvmasum2  24915  dchrisum0re  24916  qrngdiv  25027  tglngval  25161  tgisline  25237  axlowdimlem9  25545  axlowdimlem12  25548  axlowdimlem13  25549  umgra1  25618  uslgra1  25664  cusgrarn  25751  cusgrafilem2  25771  sizeusglecusglem1  25775  nbhashuvtx  26206  umgrabi  26273  2pthfrgra  26301  3cyclfrgrarn1  26302  n4cyclfrgra  26308  numclwwlk5  26402  suppss3  28693  xdivval  28761  xrge0tsmsd  28919  submatminr1  29007  ordtconlem1  29101  ispisys2  29346  sigapisys  29348  sibfinima  29531  sseqf  29584  signswch  29767  signstfvn  29775  signsvtn0  29776  signstfvcl  29779  signstfveq0a  29782  signstfveq0  29783  signsvfn  29788  signsvtp  29789  signsvtn  29790  signsvfpn  29791  signsvfnn  29792  signlem0  29793  bnj158  29854  bnj168  29855  bnj529  29868  bnj906  30057  bnj970  30074  subfacp1lem5  30223  cvmsi  30304  cvmsval  30305  cvmsdisj  30309  cvmscld  30312  cvmsss2  30313  sinccvglem  30623  circum  30625  unbdqndv2lem2  31474  lindsenlbs  32374  matunitlindflem2  32376  matunitlindf  32377  poimirlem6  32385  poimirlem7  32386  poimirlem8  32387  poimirlem16  32395  poimirlem18  32397  poimirlem19  32398  poimirlem21  32400  poimirlem22  32401  poimirlem24  32403  poimirlem25  32404  poimirlem26  32405  poimirlem27  32406  itg2addnclem2  32432  sdclem1  32509  rrncmslem  32601  rrnequiv  32604  isdrngo2  32727  isdrngo3  32728  prtlem100  32961  prter2  32984  prter3  32985  lsatlspsn2  33097  lsateln0  33100  lsatn0  33104  lsatspn0  33105  lsatcmp  33108  lsatelbN  33111  islshpat  33122  lsat0cv  33138  lkrlspeqN  33276  dvheveccl  35219  dihlatat  35444  dochnel  35500  dihjat1  35536  dvh4dimlem  35550  dochsnkr2cl  35581  dochkr1  35585  dochkr1OLDN  35586  lcfl6lem  35605  lcfl9a  35612  lclkrlem2l  35625  lclkrlem2o  35628  lclkrlem2q  35630  lcfrlem9  35657  lcfrlem16  35665  lcfrlem17  35666  lcfrlem27  35676  lcfrlem37  35686  lcfrlem38  35687  lcfrlem40  35689  lcdlkreqN  35729  mapdrvallem2  35752  mapdn0  35776  mapdpglem20  35798  mapdpglem30  35809  mapdindp0  35826  mapdhcl  35834  mapdh6aN  35842  mapdh6dN  35846  mapdh6eN  35847  mapdh6kN  35853  mapdh8  35896  hdmap1l6a  35917  hdmap1l6d  35921  hdmap1l6e  35922  hdmap1l6k  35928  hdmapval3N  35948  hdmap10  35950  hdmap11lem2  35952  hdmapnzcl  35955  hdmaprnlem3eN  35968  hdmaprnlem17N  35973  hdmap14lem4a  35981  hdmap14lem7  35984  hdmap14lem14  35991  hgmaprnlem5N  36010  hdmaplkr  36023  hdmapip0  36025  hgmapvvlem2  36034  hgmapvvlem3  36035  hgmapvv  36036  pellexlem5  36215  dfac11  36450  dfacbasgrp  36497  dgraalem  36534  dgraaub  36537  aaitgo  36551  sdrgacs  36590  cntzsdrg  36591  proot1ex  36598  isdomn3  36601  deg1mhm  36604  ofdivrec  37347  ofdivcan4  37348  ofdivdiv2  37349  expgrowth  37356  binomcxplemnotnn0  37377  dvrecg  38601  dvmptdiv  38608  dvdivbd  38614  dvdivcncf  38618  dirkeritg  38796  fourierdlem39  38840  fourierdlem57  38857  fourierdlem58  38858  fourierdlem59  38859  fourierdlem68  38868  fourierdlem76  38876  fourierdlem103  38903  fourierdlem104  38904  fourierdlem111  38911  odz2prm2pw  39815  fmtnoprmfac1  39817  fmtnoprmfac2  39819  sfprmdvdsmersenne  39860  lighneallem2  39863  lighneallem3  39864  lighneal  39868  oddprmALTV  39938  evenprm2  39963  oddprmne2  39964  elpwdifsn  40114  prprrab  40194  upgrbi  40318  upgr1elem  40336  umgrislfupgrlem  40346  edgupgr  40366  upgredg  40369  subgruhgredgd  40507  nbgrel  40563  nbupgr  40565  nbupgrel  40566  nbumgrvtx  40567  nbgrssovtx  40585  nbupgrres  40591  nbusgrvtxm1uvtx  40631  nbupgruvtxres  40633  iscplgredg  40638  cusgredg  40645  cusgrexi  40661  cusgrfilem2  40671  usgredgsscusgredg  40674  1loopgrnb0  40716  1egrvtxdg0  40726  uhgrvd00  40749  eupth2lem3lem3  41397  frcond1  41437  2pthfrgr  41453  3cyclfrgrrn1  41454  n4cyclfrgr  41460  av-numclwwlk5  41541  2zrngnmrid  41739  fdmdifeqresdif  41912  lincext1  42036  lindslinindsimp2lem5  42044  rege1logbrege0  42149  fllogbd  42151  relogbmulbexp  42152  relogbdivb  42153  nnpw2blen  42171  blennngt2o2  42183  blennn0e2  42185  dignn0ldlem  42193  aacllem  42316
  Copyright terms: Public domain W3C validator