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

Theorem eldifsn 3749
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 3162 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  -.  A  e.  { C } ) )
2 elsncg 3662 . . . 4  |-  ( A  e.  B  ->  ( A  e.  { C } 
<->  A  =  C ) )
32necon3bbid 2480 . . 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 1684    =/= wne 2446    \ cdif 3149   {csn 3640
This theorem is referenced by:  eldifsni  3750  rexdifsn  3753  difsn  3755  onmindif2  4603  sossfld  5120  fnniniseg2  5649  rexsupp  5650  suppss  5658  suppssr  5659  suppssfv  6074  suppssov1  6075  dif1o  6499  difsnen  6944  limenpsi  7036  frfi  7102  fofinf1o  7137  wemapso2  7267  dfac8clem  7659  acni2  7673  acndom  7678  acnnum  7679  dfac9  7762  dfacacn  7767  kmlem3  7778  kmlem4  7779  fin23lem21  7965  canthp1lem2  8275  elni  8500  mulnzcnopr  9414  divval  9426  elnnne0  9979  elq  10318  expcl2lem  11115  expclzlem  11127  reccn2  12070  rlimdiv  12119  eff2  12379  tanval  12408  rpnnen2lem9  12501  fzo0dvdseq  12581  4sqlem19  13010  prmlem0  13107  prmlem1a  13108  setsnid  13188  grpinvnzcl  14540  odcau  14915  efgsf  15038  efgsrel  15043  efgs1  15044  efgs1b  15045  efgsp1  15046  efgsres  15047  efgredlema  15049  efgredlemd  15053  efgrelexlemb  15059  gsumpt  15222  dmdprdd  15237  dprdcntz  15243  dprdfeq0  15257  dprd2da  15277  drngunit  15517  isdrng2  15522  drngid2  15528  isdrngd  15537  issubdrg  15570  abvtriv  15606  islss  15692  lssneln0  15709  lssssr  15710  lbsind  15833  lbspss  15835  lspabs3  15874  lspsneq  15875  lspfixed  15881  lspexch  15882  islbs2  15907  rrgsupp  16032  isdomn2  16040  domnrrg  16041  mvrcl  16193  coe1tmmul2  16352  cnflddiv  16404  cnfldinv  16405  xrs1mnd  16409  xrs10  16410  xrge0subm  16412  cnsubdrglem  16422  cnmsubglem  16434  gzrngunit  16437  zrngunit  16438  domnchr  16486  ist1-2  17075  cmpfi  17135  2ndcdisj  17182  2ndcsep  17185  alexsublem  17738  cldsubg  17793  imasdsf1olem  17937  prdsxmslem2  18075  reperflem  18323  xrge0gsumle  18338  xrge0tsms  18339  divcn  18372  evth  18457  cphreccllem  18614  bcthlem5  18750  itg11  19046  i1fmullem  19049  i1fadd  19050  itg1addlem2  19052  i1fmulc  19058  itg1mulc  19059  ellimc3  19229  limcmpt2  19234  dvlem  19246  dvidlem  19265  dvcnp  19268  dvcobr  19295  dvrec  19304  dvcnvlem  19323  dvexp3  19325  dveflem  19326  dvferm1lem  19331  dvferm2lem  19333  lhop1lem  19360  ftc1lem5  19387  mdegleb  19450  coe1mul3  19485  ply1nz  19507  fta1blem  19554  fta1b  19555  ig1peu  19557  ig1pdvds  19562  plyeq0lem  19592  dgrub  19616  quotval  19672  fta1lem  19687  fta1  19688  elqaalem3  19701  qaa  19703  iaa  19705  aareccl  19706  aannenlem2  19709  abelthlem8  19815  abelth  19817  reefgim  19826  eff1olem  19910  logrncl  19925  eflog  19933  logeftb  19937  logdmss  19989  dvlog  19998  angval  20099  dcubic  20142  rlimcnp  20260  efrlim  20264  logexprlim  20464  dchrghm  20495  dchrabs  20499  lgsfcl2  20541  lgsval2lem  20545  lgsval3  20553  lgsmod  20560  lgsdirprm  20568  lgsne0  20572  lgsquad2lem2  20598  2sqlem11  20614  2sqblem  20616  dchrvmaeq0  20653  rpvmasum2  20661  dchrisum0re  20662  qrngdiv  20773  ablomul  21022  mulid  21023  xdivval  23102  xrge0tsmsd  23382  logbcl  23399  logbid1  23400  rnlogbval  23402  relogbcl  23404  logb1  23405  nnlogbexp  23406  dmgmseqn0  23696  subfacp1lem5  23715  cvmsi  23796  cvmsval  23797  cvmsdisj  23801  cvmscld  23804  cvmsss2  23805  umgra1  23878  umgrabi  23907  sinccvglem  24005  circum  24007  axlowdimlem9  24578  axlowdimlem12  24581  axlowdimlem13  24582  divclcvd  25694  divclrvd  25695  locfincmp  26304  sdclem1  26453  rrncmslem  26556  rrnequiv  26559  isdrngo2  26589  isdrngo3  26590  prtlem100  26721  prter2  26749  prter3  26750  raldifsni  26753  pellexlem5  26918  dfac11  27160  dfacbasgrp  27273  lindfind  27286  lindsind  27287  lindff1  27290  lindfrn  27291  dgraalem  27350  dgraaub  27353  aaitgo  27367  en2eleq  27381  en2other2  27382  f1omvdmvd  27386  pmtrprfv  27396  cnmsgngrp  27436  sdrgacs  27509  cntzsdrg  27510  proot1ex  27520  isdomn3  27523  deg1mhm  27526  ofdivrec  27543  ofdivcan4  27544  ofdivdiv2  27545  expgrowth  27552  uslgra1  28118  usgra1  28119  bnj158  28757  bnj168  28758  bnj529  28770  bnj906  28962  bnj970  28979  lsatlspsn2  29182  lsateln0  29185  lsatn0  29189  lsatspn0  29190  lsatcmp  29193  lsatelbN  29196  islshpat  29207  lsat0cv  29223  lkrlspeqN  29361  dvheveccl  31302  dihlatat  31527  dochnel  31583  dihjat1  31619  dvh4dimlem  31633  dochsnkr2cl  31664  dochkr1  31668  dochkr1OLDN  31669  lcfl6lem  31688  lcfl9a  31695  lclkrlem2l  31708  lclkrlem2o  31711  lclkrlem2q  31713  lcfrlem9  31740  lcfrlem16  31748  lcfrlem17  31749  lcfrlem27  31759  lcfrlem37  31769  lcfrlem38  31770  lcfrlem40  31772  lcdlkreqN  31812  mapdrvallem2  31835  mapdn0  31859  mapdpglem20  31881  mapdpglem30  31892  mapdindp0  31909  mapdhcl  31917  mapdh6aN  31925  mapdh6dN  31929  mapdh6eN  31930  mapdh6kN  31936  mapdh8  31979  hdmap1l6a  32000  hdmap1l6d  32004  hdmap1l6e  32005  hdmap1l6k  32011  hdmapval3N  32031  hdmap10  32033  hdmap11lem2  32035  hdmapnzcl  32038  hdmaprnlem3eN  32051  hdmaprnlem17N  32056  hdmap14lem4a  32064  hdmap14lem7  32067  hdmap14lem14  32074  hgmaprnlem5N  32093  hdmaplkr  32106  hdmapip0  32108  hgmapvvlem2  32117  hgmapvvlem3  32118  hgmapvv  32119
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-v 2790  df-dif 3155  df-sn 3646
  Copyright terms: Public domain W3C validator