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

Theorem eldifsn 3988
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 3326 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  -.  A  e.  { C } ) )
2 elsncg 3888 . . . 4  |-  ( A  e.  B  ->  ( A  e.  { C } 
<->  A  =  C ) )
32necon3bbid 2632 . . 3  |-  ( A  e.  B  ->  ( -.  A  e.  { C } 
<->  A  =/=  C ) )
43pm5.32i 630 . 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 1755    =/= wne 2596    \ cdif 3313   {csn 3865
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-v 2964  df-dif 3319  df-sn 3866
This theorem is referenced by:  eldifsni  3989  rexdifsn  3992  raldifsni  3993  eldifvsn  3994  difsn  3996  sossfld  5273  fnniniseg2OLD  5815  rexsuppOLD  5816  suppssOLD  5824  suppssrOLD  5825  mpt2difsnif  6172  suppssfvOLD  6305  suppssov1OLD  6306  onmindif2  6412  mptsuppd  6701  suppssr  6709  suppssov1  6710  suppsssn  6713  suppssfv  6714  dif1o  6928  difsnen  7381  limenpsi  7474  frfi  7545  fofinf1o  7580  wemapso2OLD  7754  wemapso2lem  7755  en2eleq  8163  en2other2  8164  dfac8clem  8190  acni2  8204  acndom  8209  acnnum  8210  dfac9  8293  dfacacn  8298  kmlem3  8309  kmlem4  8310  fin23lem21  8496  canthp1lem2  8807  elni  9032  mulnzcnopr  9969  divval  9983  elnnne0  10580  elq  10942  expcl2lem  11860  expclzlem  11872  reccn2  13057  rlimdiv  13106  eff2  13365  tanval  13394  rpnnen2lem9  13487  fzo0dvdseq  13568  4sqlem19  14006  prmlem0  14115  prmlem1a  14116  setsnid  14198  grpinvnzcl  15577  symgextf  15901  symgextfv  15902  f1omvdmvd  15928  pmtrprfv  15938  odcau  16082  efgsf  16205  efgsrel  16210  efgs1  16211  efgs1b  16212  efgsp1  16213  efgsres  16214  efgredlema  16216  efgredlemd  16220  efgrelexlemb  16226  gsumpt  16428  gsumptOLD  16429  dmdprdd  16454  dprdcntz  16465  dprdfeq0  16485  dprdfeq0OLD  16492  dprd2da  16514  drngunit  16760  isdrng2  16765  drngid2  16771  isdrngd  16780  issubdrg  16813  abvtriv  16849  islss  16937  lssneln0  16954  lssssr  16955  lbsind  17082  lbspss  17084  lspabs3  17123  lspsneq  17124  lspfixed  17130  lspexch  17131  islbs2  17156  rrgsuppOLD  17284  isdomn2  17292  domnrrg  17293  mvrcl  17461  coe1tmmul2  17626  cnflddiv  17689  cnfldinv  17690  xrs1mnd  17694  xrs10  17695  xrge0subm  17697  cnsubdrglem  17707  cnmsubglem  17718  gzrngunit  17721  zringunit  17755  zrngunit  17756  domnchr  17804  cnmsgngrp  17850  psgninv  17853  psgndiflemB  17871  lindfind  18086  lindsind  18087  lindff1  18090  lindfrn  18091  mdetunilem9  18267  maducoeval2  18287  gsummatr01lem4  18305  ist1-2  18792  cmpfi  18852  2ndcdisj  18901  2ndcsep  18904  alexsublem  19457  cldsubg  19522  imasdsf1olem  19789  prdsxmslem2  19945  reperflem  20236  xrge0gsumle  20251  xrge0tsms  20252  divcn  20285  evth  20372  cvsdiv  20522  cvsdivcl  20523  cphreccllem  20538  bcthlem5  20680  itg11  21010  i1fmullem  21013  i1fadd  21014  itg1addlem2  21016  i1fmulc  21022  itg1mulc  21023  ellimc3  21195  limcmpt2  21200  dvlem  21212  dvidlem  21231  dvcnp  21234  dvcobr  21261  dvrec  21270  dvcnvlem  21289  dvexp3  21291  dveflem  21292  dvferm1lem  21297  dvferm2lem  21299  lhop1lem  21326  ftc1lem5  21353  mdegleb  21419  coe1mul3  21455  ply1nz  21477  fta1blem  21524  fta1b  21525  ig1peu  21527  ig1pdvds  21532  plyeq0lem  21562  dgrub  21586  quotval  21642  fta1lem  21657  fta1  21658  elqaalem3  21671  qaa  21673  iaa  21675  aareccl  21676  aannenlem2  21679  abelthlem8  21788  abelth  21790  reefgim  21799  eff1olem  21888  logrncl  21903  eflog  21912  logeftb  21916  logdmss  21971  dvlog  21980  angval  22081  dcubic  22125  rlimcnp  22243  efrlim  22247  logexprlim  22448  dchrghm  22479  dchrabs  22483  lgsfcl2  22525  lgsval2lem  22529  lgsval3  22537  lgsmod  22544  lgsdirprm  22552  lgsne0  22556  lgsquad2lem2  22582  2sqlem11  22598  2sqblem  22600  dchrvmaeq0  22637  rpvmasum2  22645  dchrisum0re  22646  qrngdiv  22757  tglngval  22863  tgisline  22905  axlowdimlem9  23018  axlowdimlem12  23021  axlowdimlem13  23022  umgra1  23082  uslgra1  23113  cusgrarn  23189  cusgrafilem2  23210  sizeusglecusglem1  23214  umgrabi  23426  ablomul  23664  mulid  23665  suppss3  25850  xdivval  25916  xrge0tsmsd  26105  ordtconlem1  26207  logbcl  26309  logbid1  26310  rnlogbval  26312  relogbcl  26314  logb1  26315  nnlogbexp  26316  sibfinima  26572  sseqf  26622  signswch  26809  signstfvn  26817  signsvtn0  26818  signstfvneq0  26820  signstfvcl  26821  signstfveq0a  26824  signstfveq0  26825  signsvfn  26830  signsvtp  26831  signsvtn  26832  signsvfpn  26833  signsvfnn  26834  signlem0  26835  subfacp1lem5  26919  cvmsi  27001  cvmsval  27002  cvmsdisj  27006  cvmscld  27009  cvmsss2  27010  sinccvglem  27163  circum  27165  itg2addnclem2  28285  locfincmp  28417  sdclem1  28480  rrncmslem  28572  rrnequiv  28575  isdrngo2  28605  isdrngo3  28606  prtlem100  28842  prter2  28868  prter3  28869  pellexlem5  29016  dfac11  29257  dfacbasgrp  29306  dgraalem  29344  dgraaub  29347  aaitgo  29361  sdrgacs  29400  cntzsdrg  29401  proot1ex  29411  isdomn3  29414  deg1mhm  29417  ofdivrec  29442  ofdivcan4  29443  ofdivdiv2  29444  expgrowth  29451  nbhashuvtx  30377  2pthfrgra  30446  3cyclfrgrarn1  30447  n4cyclfrgra  30453  fdmdifeqresdif  30573  lincext1  30694  lindslinindsimp2lem5  30702  bnj158  31419  bnj168  31420  bnj529  31432  bnj906  31622  bnj970  31639  lsatlspsn2  32207  lsateln0  32210  lsatn0  32214  lsatspn0  32215  lsatcmp  32218  lsatelbN  32221  islshpat  32232  lsat0cv  32248  lkrlspeqN  32386  dvheveccl  34327  dihlatat  34552  dochnel  34608  dihjat1  34644  dvh4dimlem  34658  dochsnkr2cl  34689  dochkr1  34693  dochkr1OLDN  34694  lcfl6lem  34713  lcfl9a  34720  lclkrlem2l  34733  lclkrlem2o  34736  lclkrlem2q  34738  lcfrlem9  34765  lcfrlem16  34773  lcfrlem17  34774  lcfrlem27  34784  lcfrlem37  34794  lcfrlem38  34795  lcfrlem40  34797  lcdlkreqN  34837  mapdrvallem2  34860  mapdn0  34884  mapdpglem20  34906  mapdpglem30  34917  mapdindp0  34934  mapdhcl  34942  mapdh6aN  34950  mapdh6dN  34954  mapdh6eN  34955  mapdh6kN  34961  mapdh8  35004  hdmap1l6a  35025  hdmap1l6d  35029  hdmap1l6e  35030  hdmap1l6k  35036  hdmapval3N  35056  hdmap10  35058  hdmap11lem2  35060  hdmapnzcl  35063  hdmaprnlem3eN  35076  hdmaprnlem17N  35081  hdmap14lem4a  35089  hdmap14lem7  35092  hdmap14lem14  35099  hgmaprnlem5N  35118  hdmaplkr  35131  hdmapip0  35133  hgmapvvlem2  35142  hgmapvvlem3  35143  hgmapvv  35144
  Copyright terms: Public domain W3C validator