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

Theorem eldifsn 3863
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 3266 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  -.  A  e.  { C } ) )
2 elsncg 3772 . . . 4  |-  ( A  e.  B  ->  ( A  e.  { C } 
<->  A  =  C ) )
32necon3bbid 2577 . . 3  |-  ( A  e.  B  ->  ( -.  A  e.  { C } 
<->  A  =/=  C ) )
43pm5.32i 619 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
51, 4bitri 241 1  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177    /\ wa 359    e. wcel 1717    =/= wne 2543    \ cdif 3253   {csn 3750
This theorem is referenced by:  eldifsni  3864  rexdifsn  3867  difsn  3869  onmindif2  4725  sossfld  5250  fnniniseg2  5786  rexsupp  5787  suppss  5795  suppssr  5796  suppssfv  6233  suppssov1  6234  dif1o  6673  difsnen  7119  limenpsi  7211  frfi  7281  fofinf1o  7316  wemapso2  7447  dfac8clem  7839  acni2  7853  acndom  7858  acnnum  7859  dfac9  7942  dfacacn  7947  kmlem3  7958  kmlem4  7959  fin23lem21  8145  canthp1lem2  8454  elni  8679  mulnzcnopr  9593  divval  9605  elnnne0  10160  elq  10501  expcl2lem  11313  expclzlem  11325  reccn2  12310  rlimdiv  12359  eff2  12620  tanval  12649  rpnnen2lem9  12742  fzo0dvdseq  12822  4sqlem19  13251  prmlem0  13348  prmlem1a  13349  setsnid  13429  grpinvnzcl  14783  odcau  15158  efgsf  15281  efgsrel  15286  efgs1  15287  efgs1b  15288  efgsp1  15289  efgsres  15290  efgredlema  15292  efgredlemd  15296  efgrelexlemb  15302  gsumpt  15465  dmdprdd  15480  dprdcntz  15486  dprdfeq0  15500  dprd2da  15520  drngunit  15760  isdrng2  15765  drngid2  15771  isdrngd  15780  issubdrg  15813  abvtriv  15849  islss  15931  lssneln0  15948  lssssr  15949  lbsind  16072  lbspss  16074  lspabs3  16113  lspsneq  16114  lspfixed  16120  lspexch  16121  islbs2  16146  rrgsupp  16271  isdomn2  16279  domnrrg  16280  mvrcl  16432  coe1tmmul2  16588  cnflddiv  16647  cnfldinv  16648  xrs1mnd  16652  xrs10  16653  xrge0subm  16655  cnsubdrglem  16665  cnmsubglem  16677  gzrngunit  16680  zrngunit  16681  domnchr  16729  ist1-2  17326  cmpfi  17386  2ndcdisj  17433  2ndcsep  17436  alexsublem  17989  cldsubg  18054  imasdsf1olem  18304  prdsxmslem2  18442  reperflem  18713  xrge0gsumle  18728  xrge0tsms  18729  divcn  18762  evth  18848  cphreccllem  19005  bcthlem5  19143  itg11  19443  i1fmullem  19446  i1fadd  19447  itg1addlem2  19449  i1fmulc  19455  itg1mulc  19456  ellimc3  19626  limcmpt2  19631  dvlem  19643  dvidlem  19662  dvcnp  19665  dvcobr  19692  dvrec  19701  dvcnvlem  19720  dvexp3  19722  dveflem  19723  dvferm1lem  19728  dvferm2lem  19730  lhop1lem  19757  ftc1lem5  19784  mdegleb  19847  coe1mul3  19882  ply1nz  19904  fta1blem  19951  fta1b  19952  ig1peu  19954  ig1pdvds  19959  plyeq0lem  19989  dgrub  20013  quotval  20069  fta1lem  20084  fta1  20085  elqaalem3  20098  qaa  20100  iaa  20102  aareccl  20103  aannenlem2  20106  abelthlem8  20215  abelth  20217  reefgim  20226  eff1olem  20310  logrncl  20325  eflog  20334  logeftb  20338  logdmss  20393  dvlog  20402  angval  20503  dcubic  20546  rlimcnp  20664  efrlim  20668  logexprlim  20869  dchrghm  20900  dchrabs  20904  lgsfcl2  20946  lgsval2lem  20950  lgsval3  20958  lgsmod  20965  lgsdirprm  20973  lgsne0  20977  lgsquad2lem2  21003  2sqlem11  21019  2sqblem  21021  dchrvmaeq0  21058  rpvmasum2  21066  dchrisum0re  21067  qrngdiv  21178  umgra1  21221  uslgra1  21252  cusgrarn  21327  cusgrafilem2  21348  sizeusglecusglem1  21352  umgrabi  21546  ablomul  21784  mulid  21785  xdivval  23996  xrge0tsmsd  24045  logbcl  24186  logbid1  24187  rnlogbval  24189  relogbcl  24191  logb1  24192  nnlogbexp  24193  subfacp1lem5  24642  cvmsi  24724  cvmsval  24725  cvmsdisj  24729  cvmscld  24732  cvmsss2  24733  sinccvglem  24881  circum  24883  axlowdimlem9  25596  axlowdimlem12  25599  axlowdimlem13  25600  itg2addnclem2  25951  locfincmp  26068  sdclem1  26131  rrncmslem  26225  rrnequiv  26228  isdrngo2  26258  isdrngo3  26259  prtlem100  26388  prter2  26414  prter3  26415  raldifsni  26418  pellexlem5  26580  dfac11  26822  dfacbasgrp  26935  lindfind  26948  lindsind  26949  lindff1  26952  lindfrn  26953  dgraalem  27012  dgraaub  27015  aaitgo  27029  en2eleq  27043  en2other2  27044  f1omvdmvd  27048  pmtrprfv  27058  cnmsgngrp  27098  sdrgacs  27171  cntzsdrg  27172  proot1ex  27182  isdomn3  27185  deg1mhm  27188  ofdivrec  27205  ofdivcan4  27206  ofdivdiv2  27207  expgrowth  27214  2pthfrgra  27757  3cyclfrgrarn1  27758  n4cyclfrgra  27764  bnj158  28427  bnj168  28428  bnj529  28440  bnj906  28632  bnj970  28649  lsatlspsn2  29158  lsateln0  29161  lsatn0  29165  lsatspn0  29166  lsatcmp  29169  lsatelbN  29172  islshpat  29183  lsat0cv  29199  lkrlspeqN  29337  dvheveccl  31278  dihlatat  31503  dochnel  31559  dihjat1  31595  dvh4dimlem  31609  dochsnkr2cl  31640  dochkr1  31644  dochkr1OLDN  31645  lcfl6lem  31664  lcfl9a  31671  lclkrlem2l  31684  lclkrlem2o  31687  lclkrlem2q  31689  lcfrlem9  31716  lcfrlem16  31724  lcfrlem17  31725  lcfrlem27  31735  lcfrlem37  31745  lcfrlem38  31746  lcfrlem40  31748  lcdlkreqN  31788  mapdrvallem2  31811  mapdn0  31835  mapdpglem20  31857  mapdpglem30  31868  mapdindp0  31885  mapdhcl  31893  mapdh6aN  31901  mapdh6dN  31905  mapdh6eN  31906  mapdh6kN  31912  mapdh8  31955  hdmap1l6a  31976  hdmap1l6d  31980  hdmap1l6e  31981  hdmap1l6k  31987  hdmapval3N  32007  hdmap10  32009  hdmap11lem2  32011  hdmapnzcl  32014  hdmaprnlem3eN  32027  hdmaprnlem17N  32032  hdmap14lem4a  32040  hdmap14lem7  32043  hdmap14lem14  32050  hgmaprnlem5N  32069  hdmaplkr  32082  hdmapip0  32084  hgmapvvlem2  32093  hgmapvvlem3  32094  hgmapvv  32095
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-v 2894  df-dif 3259  df-sn 3756
  Copyright terms: Public domain W3C validator