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

Theorem eldifsn 4110
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 3426 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  -.  A  e.  { C } ) )
2 elsncg 4003 . . . 4  |-  ( A  e.  B  ->  ( A  e.  { C } 
<->  A  =  C ) )
32necon3bbid 2673 . . 3  |-  ( A  e.  B  ->  ( -.  A  e.  { C } 
<->  A  =/=  C ) )
43pm5.32i 647 . 2  |-  ( ( A  e.  B  /\  -.  A  e.  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
51, 4bitri 257 1  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  A  =/= 
C ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 189    /\ wa 375    e. wcel 1898    =/= wne 2633    \ cdif 3413   {csn 3980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-v 3059  df-dif 3419  df-sn 3981
This theorem is referenced by:  eldifsni  4111  rexdifsn  4114  raldifsni  4115  eldifvsn  4117  difsn  4119  sossfld  5305  tpres  6146  mpt2difsnif  6421  onmindif2  6671  mptsuppd  6970  suppssr  6978  suppssov1  6979  suppsssn  6982  suppssfv  6983  dif1o  7233  difsnen  7685  limenpsi  7778  frfi  7847  fofinf1o  7883  wemapso2lem  8098  en2eleq  8470  en2other2  8471  dfac8clem  8494  acni2  8508  acndom  8513  acnnum  8514  dfac9  8597  dfacacn  8602  kmlem3  8613  kmlem4  8614  fin23lem21  8800  canthp1lem2  9109  elni  9332  mulnzcnopr  10291  divval  10305  elnnne0  10917  elq  11300  rpcndif0  11354  expcl2lem  12322  expclzlem  12334  hashdifpr  12630  reccn2  13715  rlimdiv  13764  eff2  14208  tanval  14237  rpnnen2lem9  14330  fzo0dvdseq  14413  4sqlem19  14968  prmlem0  15132  prmlem1a  15133  setsnid  15220  grpinvnzcl  16781  symgextf  17113  symgextfv  17114  f1omvdmvd  17139  pmtrprfv  17149  odcau  17311  efgsf  17434  efgsrel  17439  efgs1  17440  efgs1b  17441  efgsp1  17442  efgsres  17443  efgredlema  17445  efgredlemd  17449  efgrelexlemb  17455  gsumpt  17649  dmdprdd  17686  dprdcntz  17695  dprdfeq0  17710  dprd2da  17730  drngunit  18035  isdrng2  18040  drngid2  18046  isdrngd  18055  issubdrg  18088  abvtriv  18124  islss  18213  lssneln0  18230  lssssr  18231  lbsind  18358  lbspss  18360  lspabs3  18399  lspsneq  18400  lspfixed  18406  lspexch  18407  islbs2  18432  isdomn2  18578  domnrrg  18579  mvrcl  18728  coe1tmmul2  18924  cnflddiv  19053  cnfldinv  19054  xrs1mnd  19061  xrs10  19062  xrge0subm  19064  cnsubdrglem  19074  cnmsubglem  19085  gzrngunit  19088  zringunit  19117  domnchr  19158  cnmsgngrp  19202  psgninv  19205  psgndiflemB  19223  lindfind  19429  lindsind  19430  lindff1  19433  lindfrn  19434  mdetunilem9  19700  maducoeval2  19720  gsummatr01lem4  19738  ist1-2  20418  cmpfi  20478  2ndcdisj  20526  2ndcsep  20529  locfincmp  20596  alexsublem  21114  cldsubg  21180  imasdsf1olem  21443  prdsxmslem2  21599  reperflem  21891  xrge0gsumle  21906  xrge0tsms  21907  divcn  21955  evth  22042  cvsdiv  22195  cvsdivcl  22196  cphreccllem  22211  bcthlem5  22351  itg11  22705  i1fmullem  22708  i1fadd  22709  itg1addlem2  22711  i1fmulc  22717  itg1mulc  22718  ellimc3  22890  limcmpt2  22895  dvlem  22907  dvidlem  22926  dvcnp  22929  dvcobr  22956  dvrec  22965  dvcnvlem  22984  dvexp3  22986  dveflem  22987  dvferm1lem  22992  dvferm2lem  22994  lhop1lem  23021  ftc1lem5  23048  mdegleb  23069  coe1mul3  23104  ply1nz  23126  fta1blem  23175  fta1b  23176  ig1peu  23178  ig1peuOLD  23179  ig1pdvds  23184  ig1pdvdsOLD  23190  plyeq0lem  23220  dgrub  23244  quotval  23301  fta1lem  23316  fta1  23317  elqaalem3  23330  elqaalem3OLD  23333  qaa  23335  iaa  23337  aareccl  23338  aannenlem2  23341  abelthlem8  23450  abelth  23452  reefgim  23461  eff1olem  23553  logrncl  23573  eflog  23582  logeftb  23589  logdmss  23643  dvlog  23652  logbcl  23760  logbid1  23761  logb1  23762  elogb  23763  logbchbase  23764  relogbval  23765  relogbcl  23766  relogbreexp  23768  relogbmul  23770  nnlogbexp  23774  relogbcxp  23778  cxplogb  23779  relogbcxpb  23780  logbf  23782  logblog  23785  angval  23786  dcubic  23828  rlimcnp  23947  efrlim  23951  logexprlim  24209  dchrghm  24240  dchrabs  24244  lgsfcl2  24286  lgsval2lem  24290  lgsval3  24298  lgsmod  24305  lgsdirprm  24313  lgsne0  24317  lgsquad2lem2  24343  2sqlem11  24359  2sqblem  24361  dchrvmaeq0  24398  rpvmasum2  24406  dchrisum0re  24407  qrngdiv  24518  tglngval  24652  tgisline  24728  axlowdimlem9  25036  axlowdimlem12  25039  axlowdimlem13  25040  umgra1  25109  uslgra1  25155  cusgrarn  25243  cusgrafilem2  25264  sizeusglecusglem1  25268  nbhashuvtx  25700  umgrabi  25767  2pthfrgra  25795  3cyclfrgrarn1  25796  n4cyclfrgra  25802  ablomul  26139  mulid  26140  suppss3  28364  xdivval  28440  xrge0tsmsd  28599  submatminr1  28687  ordtconlem1  28781  ispisys2  29026  sigapisys  29028  sibfinima  29222  sseqf  29275  signswch  29500  signstfvn  29508  signsvtn0  29509  signstfvcl  29512  signstfveq0a  29515  signstfveq0  29516  signsvfn  29521  signsvtp  29522  signsvtn  29523  signsvfpn  29524  signsvfnn  29525  signlem0  29526  bnj158  29587  bnj168  29588  bnj529  29601  bnj906  29791  bnj970  29808  subfacp1lem5  29957  cvmsi  30038  cvmsval  30039  cvmsdisj  30043  cvmscld  30046  cvmsss2  30047  sinccvglem  30366  circum  30368  poimirlem6  31992  poimirlem7  31993  poimirlem8  31994  poimirlem16  32002  poimirlem18  32004  poimirlem19  32005  poimirlem21  32007  poimirlem22  32008  poimirlem24  32010  poimirlem25  32011  poimirlem26  32012  poimirlem27  32013  itg2addnclem2  32040  sdclem1  32118  rrncmslem  32210  rrnequiv  32213  isdrngo2  32243  isdrngo3  32244  prtlem100  32475  prter2  32499  prter3  32500  lsatlspsn2  32604  lsateln0  32607  lsatn0  32611  lsatspn0  32612  lsatcmp  32615  lsatelbN  32618  islshpat  32629  lsat0cv  32645  lkrlspeqN  32783  dvheveccl  34726  dihlatat  34951  dochnel  35007  dihjat1  35043  dvh4dimlem  35057  dochsnkr2cl  35088  dochkr1  35092  dochkr1OLDN  35093  lcfl6lem  35112  lcfl9a  35119  lclkrlem2l  35132  lclkrlem2o  35135  lclkrlem2q  35137  lcfrlem9  35164  lcfrlem16  35172  lcfrlem17  35173  lcfrlem27  35183  lcfrlem37  35193  lcfrlem38  35194  lcfrlem40  35196  lcdlkreqN  35236  mapdrvallem2  35259  mapdn0  35283  mapdpglem20  35305  mapdpglem30  35316  mapdindp0  35333  mapdhcl  35341  mapdh6aN  35349  mapdh6dN  35353  mapdh6eN  35354  mapdh6kN  35360  mapdh8  35403  hdmap1l6a  35424  hdmap1l6d  35428  hdmap1l6e  35429  hdmap1l6k  35435  hdmapval3N  35455  hdmap10  35457  hdmap11lem2  35459  hdmapnzcl  35462  hdmaprnlem3eN  35475  hdmaprnlem17N  35480  hdmap14lem4a  35488  hdmap14lem7  35491  hdmap14lem14  35498  hgmaprnlem5N  35517  hdmaplkr  35530  hdmapip0  35532  hgmapvvlem2  35541  hgmapvvlem3  35542  hgmapvv  35543  pellexlem5  35723  dfac11  35966  dfacbasgrp  36013  dgraalem  36053  dgraalemOLD  36054  dgraaub  36059  dgraaubOLD  36060  aaitgo  36074  sdrgacs  36113  cntzsdrg  36114  proot1ex  36124  isdomn3  36127  deg1mhm  36130  ofdivrec  36720  ofdivcan4  36721  ofdivdiv2  36722  expgrowth  36729  binomcxplemnotnn0  36750  dvrecg  37868  dvmptdiv  37875  dvdivbd  37881  dvdivcncf  37885  dirkeritg  38065  fourierdlem39  38110  fourierdlem57  38128  fourierdlem58  38129  fourierdlem59  38130  fourierdlem68  38139  fourierdlem76  38147  fourierdlem103  38174  fourierdlem104  38175  fourierdlem111  38182  oddprmALTV  38951  evenprm2  38977  elpwdifsn  39127  prprrab  39210  upgr1elem  39344  edgupgr  39369  upgredg  39372  subgruhgredgd  39502  nbgrel  39556  nbupgr  39558  nbupgrel  39559  nbumgrvtx  39560  nbgrssovtx  39578  nbupgrres  39584  nbusgrvtxm1uvtx  39624  nbupgruvtxres  39626  iscplgredg  39631  cusgredg  39638  cusgrexi  39653  cusgrfilem2  39663  usgredgsscusgredg  39666  uspgrloopnb0  39702  uhgrvd00  39717  umgrislfupgrlem  39814  2zrngnmrid  40319  fdmdifeqresdif  40492  lincext1  40616  lindslinindsimp2lem5  40624  rege1logbrege0  40738  fllogbd  40740  relogbmulbexp  40741  relogbdivb  40742  nnpw2blen  40760  blennngt2o2  40772  blennn0e2  40774  dignn0ldlem  40782  aacllem  40909
  Copyright terms: Public domain W3C validator