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

Theorem eldifsn 3762
Description: Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
Assertion
Ref Expression
eldifsn  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )

Proof of Theorem eldifsn
StepHypRef Expression
1 eldif 3175 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  -.  A  e.  { C } ) )
2 elsncg 3675 . . . 4  |-  ( A  e.  B  ->  ( A  e.  { C } 
<->  A  =  C ) )
32necon3bbid 2493 . . 3  |-  ( A  e.  B  ->  ( -.  A  e.  { C } 
<->  A  =/=  C ) )
43pm5.32i 618 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
51, 4bitri 240 1  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    /\ wa 358    e. wcel 1696    =/= wne 2459    \ cdif 3162   {csn 3653
This theorem is referenced by:  eldifsni  3763  rexdifsn  3766  difsn  3768  onmindif2  4619  sossfld  5136  fnniniseg2  5665  rexsupp  5666  suppss  5674  suppssr  5675  suppssfv  6090  suppssov1  6091  dif1o  6515  difsnen  6960  limenpsi  7052  frfi  7118  fofinf1o  7153  wemapso2  7283  dfac8clem  7675  acni2  7689  acndom  7694  acnnum  7695  dfac9  7778  dfacacn  7783  kmlem3  7794  kmlem4  7795  fin23lem21  7981  canthp1lem2  8291  elni  8516  mulnzcnopr  9430  divval  9442  elnnne0  9995  elq  10334  expcl2lem  11131  expclzlem  11143  reccn2  12086  rlimdiv  12135  eff2  12395  tanval  12424  rpnnen2lem9  12517  fzo0dvdseq  12597  4sqlem19  13026  prmlem0  13123  prmlem1a  13124  setsnid  13204  grpinvnzcl  14556  odcau  14931  efgsf  15054  efgsrel  15059  efgs1  15060  efgs1b  15061  efgsp1  15062  efgsres  15063  efgredlema  15065  efgredlemd  15069  efgrelexlemb  15075  gsumpt  15238  dmdprdd  15253  dprdcntz  15259  dprdfeq0  15273  dprd2da  15293  drngunit  15533  isdrng2  15538  drngid2  15544  isdrngd  15553  issubdrg  15586  abvtriv  15622  islss  15708  lssneln0  15725  lssssr  15726  lbsind  15849  lbspss  15851  lspabs3  15890  lspsneq  15891  lspfixed  15897  lspexch  15898  islbs2  15923  rrgsupp  16048  isdomn2  16056  domnrrg  16057  mvrcl  16209  coe1tmmul2  16368  cnflddiv  16420  cnfldinv  16421  xrs1mnd  16425  xrs10  16426  xrge0subm  16428  cnsubdrglem  16438  cnmsubglem  16450  gzrngunit  16453  zrngunit  16454  domnchr  16502  ist1-2  17091  cmpfi  17151  2ndcdisj  17198  2ndcsep  17201  alexsublem  17754  cldsubg  17809  imasdsf1olem  17953  prdsxmslem2  18091  reperflem  18339  xrge0gsumle  18354  xrge0tsms  18355  divcn  18388  evth  18473  cphreccllem  18630  bcthlem5  18766  itg11  19062  i1fmullem  19065  i1fadd  19066  itg1addlem2  19068  i1fmulc  19074  itg1mulc  19075  ellimc3  19245  limcmpt2  19250  dvlem  19262  dvidlem  19281  dvcnp  19284  dvcobr  19311  dvrec  19320  dvcnvlem  19339  dvexp3  19341  dveflem  19342  dvferm1lem  19347  dvferm2lem  19349  lhop1lem  19376  ftc1lem5  19403  mdegleb  19466  coe1mul3  19501  ply1nz  19523  fta1blem  19570  fta1b  19571  ig1peu  19573  ig1pdvds  19578  plyeq0lem  19608  dgrub  19632  quotval  19688  fta1lem  19703  fta1  19704  elqaalem3  19717  qaa  19719  iaa  19721  aareccl  19722  aannenlem2  19725  abelthlem8  19831  abelth  19833  reefgim  19842  eff1olem  19926  logrncl  19941  eflog  19949  logeftb  19953  logdmss  20005  dvlog  20014  angval  20115  dcubic  20158  rlimcnp  20276  efrlim  20280  logexprlim  20480  dchrghm  20511  dchrabs  20515  lgsfcl2  20557  lgsval2lem  20561  lgsval3  20569  lgsmod  20576  lgsdirprm  20584  lgsne0  20588  lgsquad2lem2  20614  2sqlem11  20630  2sqblem  20632  dchrvmaeq0  20669  rpvmasum2  20677  dchrisum0re  20678  qrngdiv  20789  ablomul  21038  mulid  21039  xdivval  23118  xrge0tsmsd  23397  logbcl  23414  logbid1  23415  rnlogbval  23417  relogbcl  23419  logb1  23420  nnlogbexp  23421  dmgmseqn0  23711  subfacp1lem5  23730  cvmsi  23811  cvmsval  23812  cvmsdisj  23816  cvmscld  23819  cvmsss2  23820  umgra1  23893  umgrabi  23922  sinccvglem  24020  circum  24022  axlowdimlem9  24649  axlowdimlem12  24652  axlowdimlem13  24653  itg2addnclem2  25003  divclcvd  25796  divclrvd  25797  locfincmp  26406  sdclem1  26555  rrncmslem  26658  rrnequiv  26661  isdrngo2  26691  isdrngo3  26692  prtlem100  26823  prter2  26851  prter3  26852  raldifsni  26855  pellexlem5  27020  dfac11  27262  dfacbasgrp  27375  lindfind  27388  lindsind  27389  lindff1  27392  lindfrn  27393  dgraalem  27452  dgraaub  27455  aaitgo  27469  en2eleq  27483  en2other2  27484  f1omvdmvd  27488  pmtrprfv  27498  cnmsgngrp  27538  sdrgacs  27611  cntzsdrg  27612  proot1ex  27622  isdomn3  27625  deg1mhm  27628  ofdivrec  27645  ofdivcan4  27646  ofdivdiv2  27647  expgrowth  27654  uslgra1  28251  usgra1  28252  3cyclfrgrarn1  28434  n4cyclfrgra  28439  bnj158  29072  bnj168  29073  bnj529  29085  bnj906  29277  bnj970  29294  lsatlspsn2  29804  lsateln0  29807  lsatn0  29811  lsatspn0  29812  lsatcmp  29815  lsatelbN  29818  islshpat  29829  lsat0cv  29845  lkrlspeqN  29983  dvheveccl  31924  dihlatat  32149  dochnel  32205  dihjat1  32241  dvh4dimlem  32255  dochsnkr2cl  32286  dochkr1  32290  dochkr1OLDN  32291  lcfl6lem  32310  lcfl9a  32317  lclkrlem2l  32330  lclkrlem2o  32333  lclkrlem2q  32335  lcfrlem9  32362  lcfrlem16  32370  lcfrlem17  32371  lcfrlem27  32381  lcfrlem37  32391  lcfrlem38  32392  lcfrlem40  32394  lcdlkreqN  32434  mapdrvallem2  32457  mapdn0  32481  mapdpglem20  32503  mapdpglem30  32514  mapdindp0  32531  mapdhcl  32539  mapdh6aN  32547  mapdh6dN  32551  mapdh6eN  32552  mapdh6kN  32558  mapdh8  32601  hdmap1l6a  32622  hdmap1l6d  32626  hdmap1l6e  32627  hdmap1l6k  32633  hdmapval3N  32653  hdmap10  32655  hdmap11lem2  32657  hdmapnzcl  32660  hdmaprnlem3eN  32673  hdmaprnlem17N  32678  hdmap14lem4a  32686  hdmap14lem7  32689  hdmap14lem14  32696  hgmaprnlem5N  32715  hdmaplkr  32728  hdmapip0  32730  hgmapvvlem2  32739  hgmapvvlem3  32740  hgmapvv  32741
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-v 2803  df-dif 3168  df-sn 3659
  Copyright terms: Public domain W3C validator