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

Theorem eldifsn 3995
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 3333 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  -.  A  e.  { C } ) )
2 elsncg 3895 . . . 4  |-  ( A  e.  B  ->  ( A  e.  { C } 
<->  A  =  C ) )
32necon3bbid 2637 . . 3  |-  ( A  e.  B  ->  ( -.  A  e.  { C } 
<->  A  =/=  C ) )
43pm5.32i 637 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
51, 4bitri 249 1  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    /\ wa 369    e. wcel 1756    =/= wne 2601    \ cdif 3320   {csn 3872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-v 2969  df-dif 3326  df-sn 3873
This theorem is referenced by:  eldifsni  3996  rexdifsn  3999  raldifsni  4000  eldifvsn  4001  difsn  4003  sossfld  5280  fnniniseg2OLD  5822  rexsuppOLD  5823  suppssOLD  5831  suppssrOLD  5832  mpt2difsnif  6178  suppssfvOLD  6311  suppssov1OLD  6312  onmindif2  6418  mptsuppd  6707  suppssr  6715  suppssov1  6716  suppsssn  6719  suppssfv  6720  dif1o  6932  difsnen  7385  limenpsi  7478  frfi  7549  fofinf1o  7584  wemapso2OLD  7758  wemapso2lem  7759  en2eleq  8167  en2other2  8168  dfac8clem  8194  acni2  8208  acndom  8213  acnnum  8214  dfac9  8297  dfacacn  8302  kmlem3  8313  kmlem4  8314  fin23lem21  8500  canthp1lem2  8812  elni  9037  mulnzcnopr  9974  divval  9988  elnnne0  10585  elq  10947  expcl2lem  11869  expclzlem  11881  reccn2  13066  rlimdiv  13115  eff2  13375  tanval  13404  rpnnen2lem9  13497  fzo0dvdseq  13578  4sqlem19  14016  prmlem0  14125  prmlem1a  14126  setsnid  14208  grpinvnzcl  15589  symgextf  15913  symgextfv  15914  f1omvdmvd  15940  pmtrprfv  15950  odcau  16094  efgsf  16217  efgsrel  16222  efgs1  16223  efgs1b  16224  efgsp1  16225  efgsres  16226  efgredlema  16228  efgredlemd  16232  efgrelexlemb  16238  gsumpt  16444  gsumptOLD  16445  dmdprdd  16471  dprdcntz  16482  dprdfeq0  16502  dprdfeq0OLD  16509  dprd2da  16531  drngunit  16817  isdrng2  16822  drngid2  16828  isdrngd  16837  issubdrg  16870  abvtriv  16906  islss  16996  lssneln0  17013  lssssr  17014  lbsind  17141  lbspss  17143  lspabs3  17182  lspsneq  17183  lspfixed  17189  lspexch  17190  islbs2  17215  rrgsuppOLD  17343  isdomn2  17351  domnrrg  17352  mvrcl  17508  coe1tmmul2  17709  cnflddiv  17826  cnfldinv  17827  xrs1mnd  17831  xrs10  17832  xrge0subm  17834  cnsubdrglem  17844  cnmsubglem  17855  gzrngunit  17858  zringunit  17894  zrngunit  17895  domnchr  17943  cnmsgngrp  17989  psgninv  17992  psgndiflemB  18010  lindfind  18225  lindsind  18226  lindff1  18229  lindfrn  18230  mdetunilem9  18406  maducoeval2  18426  gsummatr01lem4  18444  ist1-2  18931  cmpfi  18991  2ndcdisj  19040  2ndcsep  19043  alexsublem  19596  cldsubg  19661  imasdsf1olem  19928  prdsxmslem2  20084  reperflem  20375  xrge0gsumle  20390  xrge0tsms  20391  divcn  20424  evth  20511  cvsdiv  20661  cvsdivcl  20662  cphreccllem  20677  bcthlem5  20819  itg11  21149  i1fmullem  21152  i1fadd  21153  itg1addlem2  21155  i1fmulc  21161  itg1mulc  21162  ellimc3  21334  limcmpt2  21339  dvlem  21351  dvidlem  21370  dvcnp  21373  dvcobr  21400  dvrec  21409  dvcnvlem  21428  dvexp3  21430  dveflem  21431  dvferm1lem  21436  dvferm2lem  21438  lhop1lem  21465  ftc1lem5  21492  mdegleb  21515  coe1mul3  21551  ply1nz  21573  fta1blem  21620  fta1b  21621  ig1peu  21623  ig1pdvds  21628  plyeq0lem  21658  dgrub  21682  quotval  21738  fta1lem  21753  fta1  21754  elqaalem3  21767  qaa  21769  iaa  21771  aareccl  21772  aannenlem2  21775  abelthlem8  21884  abelth  21886  reefgim  21895  eff1olem  21984  logrncl  21999  eflog  22008  logeftb  22012  logdmss  22067  dvlog  22076  angval  22177  dcubic  22221  rlimcnp  22339  efrlim  22343  logexprlim  22544  dchrghm  22575  dchrabs  22579  lgsfcl2  22621  lgsval2lem  22625  lgsval3  22633  lgsmod  22640  lgsdirprm  22648  lgsne0  22652  lgsquad2lem2  22678  2sqlem11  22694  2sqblem  22696  dchrvmaeq0  22733  rpvmasum2  22741  dchrisum0re  22742  qrngdiv  22853  tglngval  22965  tgisline  23014  axlowdimlem9  23168  axlowdimlem12  23171  axlowdimlem13  23172  umgra1  23232  uslgra1  23263  cusgrarn  23339  cusgrafilem2  23360  sizeusglecusglem1  23364  umgrabi  23576  ablomul  23814  mulid  23815  suppss3  25999  xdivval  26066  xrge0tsmsd  26225  ordtconlem1  26327  logbcl  26429  logbid1  26430  rnlogbval  26432  relogbcl  26434  logb1  26435  nnlogbexp  26436  sibfinima  26698  sseqf  26748  signswch  26935  signstfvn  26943  signsvtn0  26944  signstfvneq0  26946  signstfvcl  26947  signstfveq0a  26950  signstfveq0  26951  signsvfn  26956  signsvtp  26957  signsvtn  26958  signsvfpn  26959  signsvfnn  26960  signlem0  26961  subfacp1lem5  27045  cvmsi  27127  cvmsval  27128  cvmsdisj  27132  cvmscld  27135  cvmsss2  27136  sinccvglem  27290  circum  27292  itg2addnclem2  28418  locfincmp  28550  sdclem1  28613  rrncmslem  28705  rrnequiv  28708  isdrngo2  28738  isdrngo3  28739  prtlem100  28974  prter2  29000  prter3  29001  pellexlem5  29148  dfac11  29389  dfacbasgrp  29438  dgraalem  29476  dgraaub  29479  aaitgo  29493  sdrgacs  29532  cntzsdrg  29533  proot1ex  29543  isdomn3  29546  deg1mhm  29549  ofdivrec  29574  ofdivcan4  29575  ofdivdiv2  29576  expgrowth  29583  nbhashuvtx  30508  2pthfrgra  30577  3cyclfrgrarn1  30578  n4cyclfrgra  30584  fdmdifeqresdif  30705  lincext1  30922  lindslinindsimp2lem5  30930  bnj158  31652  bnj168  31653  bnj529  31665  bnj906  31855  bnj970  31872  lsatlspsn2  32554  lsateln0  32557  lsatn0  32561  lsatspn0  32562  lsatcmp  32565  lsatelbN  32568  islshpat  32579  lsat0cv  32595  lkrlspeqN  32733  dvheveccl  34674  dihlatat  34899  dochnel  34955  dihjat1  34991  dvh4dimlem  35005  dochsnkr2cl  35036  dochkr1  35040  dochkr1OLDN  35041  lcfl6lem  35060  lcfl9a  35067  lclkrlem2l  35080  lclkrlem2o  35083  lclkrlem2q  35085  lcfrlem9  35112  lcfrlem16  35120  lcfrlem17  35121  lcfrlem27  35131  lcfrlem37  35141  lcfrlem38  35142  lcfrlem40  35144  lcdlkreqN  35184  mapdrvallem2  35207  mapdn0  35231  mapdpglem20  35253  mapdpglem30  35264  mapdindp0  35281  mapdhcl  35289  mapdh6aN  35297  mapdh6dN  35301  mapdh6eN  35302  mapdh6kN  35308  mapdh8  35351  hdmap1l6a  35372  hdmap1l6d  35376  hdmap1l6e  35377  hdmap1l6k  35383  hdmapval3N  35403  hdmap10  35405  hdmap11lem2  35407  hdmapnzcl  35410  hdmaprnlem3eN  35423  hdmaprnlem17N  35428  hdmap14lem4a  35436  hdmap14lem7  35439  hdmap14lem14  35446  hgmaprnlem5N  35465  hdmaplkr  35478  hdmapip0  35480  hgmapvvlem2  35489  hgmapvvlem3  35490  hgmapvv  35491
  Copyright terms: Public domain W3C validator