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

Theorem eldifsn 4069
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 3399 . 2  |-  ( A  e.  ( B  \  { C } )  <->  ( A  e.  B  /\  -.  A  e.  { C } ) )
2 elsncg 3967 . . . 4  |-  ( A  e.  B  ->  ( A  e.  { C } 
<->  A  =  C ) )
32necon3bbid 2629 . . 3  |-  ( A  e.  B  ->  ( -.  A  e.  { C } 
<->  A  =/=  C ) )
43pm5.32i 635 . 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 367    e. wcel 1826    =/= wne 2577    \ cdif 3386   {csn 3944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-v 3036  df-dif 3392  df-sn 3945
This theorem is referenced by:  eldifsni  4070  rexdifsn  4073  raldifsni  4074  eldifvsn  4076  difsn  4078  sossfld  5363  fnniniseg2OLD  5913  rexsuppOLD  5914  suppssOLD  5922  suppssrOLD  5923  tpres  6026  mpt2difsnif  6294  suppssfvOLD  6430  suppssov1OLD  6431  onmindif2  6546  mptsuppd  6841  suppssr  6849  suppssov1  6850  suppsssn  6853  suppssfv  6854  dif1o  7068  difsnen  7518  limenpsi  7611  frfi  7680  fofinf1o  7716  wemapso2OLD  7892  wemapso2lem  7893  en2eleq  8299  en2other2  8300  dfac8clem  8326  acni2  8340  acndom  8345  acnnum  8346  dfac9  8429  dfacacn  8434  kmlem3  8445  kmlem4  8446  fin23lem21  8632  canthp1lem2  8942  elni  9165  mulnzcnopr  10112  divval  10126  elnnne0  10726  elq  11103  rpcndif0  11157  expcl2lem  12081  expclzlem  12093  reccn2  13421  rlimdiv  13470  eff2  13836  tanval  13865  rpnnen2lem9  13958  fzo0dvdseq  14041  4sqlem19  14483  prmlem0  14593  prmlem1a  14594  setsnid  14678  grpinvnzcl  16227  symgextf  16559  symgextfv  16560  f1omvdmvd  16585  pmtrprfv  16595  odcau  16741  efgsf  16864  efgsrel  16869  efgs1  16870  efgs1b  16871  efgsp1  16872  efgsres  16873  efgredlema  16875  efgredlemd  16879  efgrelexlemb  16885  gsumpt  17102  gsumptOLD  17103  dmdprdd  17143  dprdcntz  17154  dprdfeq0  17175  dprdfeq0OLD  17182  dprd2da  17204  drngunit  17514  isdrng2  17519  drngid2  17525  isdrngd  17534  issubdrg  17567  abvtriv  17603  islss  17694  lssneln0  17711  lssssr  17712  lbsind  17839  lbspss  17841  lspabs3  17880  lspsneq  17881  lspfixed  17887  lspexch  17888  islbs2  17913  rrgsuppOLD  18053  isdomn2  18061  domnrrg  18062  mvrcl  18224  coe1tmmul2  18430  cnflddiv  18561  cnfldinv  18562  xrs1mnd  18569  xrs10  18570  xrge0subm  18572  cnsubdrglem  18582  cnmsubglem  18593  gzrngunit  18596  zringunit  18621  domnchr  18662  cnmsgngrp  18706  psgninv  18709  psgndiflemB  18727  lindfind  18936  lindsind  18937  lindff1  18940  lindfrn  18941  mdetunilem9  19207  maducoeval2  19227  gsummatr01lem4  19245  ist1-2  19934  cmpfi  19994  2ndcdisj  20042  2ndcsep  20045  locfincmp  20112  alexsublem  20629  cldsubg  20694  imasdsf1olem  20961  prdsxmslem2  21117  reperflem  21408  xrge0gsumle  21423  xrge0tsms  21424  divcn  21457  evth  21544  cvsdiv  21694  cvsdivcl  21695  cphreccllem  21710  bcthlem5  21852  itg11  22183  i1fmullem  22186  i1fadd  22187  itg1addlem2  22189  i1fmulc  22195  itg1mulc  22196  ellimc3  22368  limcmpt2  22373  dvlem  22385  dvidlem  22404  dvcnp  22407  dvcobr  22434  dvrec  22443  dvcnvlem  22462  dvexp3  22464  dveflem  22465  dvferm1lem  22470  dvferm2lem  22472  lhop1lem  22499  ftc1lem5  22526  mdegleb  22549  coe1mul3  22585  ply1nz  22607  fta1blem  22654  fta1b  22655  ig1peu  22657  ig1pdvds  22662  plyeq0lem  22692  dgrub  22716  quotval  22773  fta1lem  22788  fta1  22789  elqaalem3  22802  qaa  22804  iaa  22806  aareccl  22807  aannenlem2  22810  abelthlem8  22919  abelth  22921  reefgim  22930  eff1olem  23020  logrncl  23040  eflog  23049  logeftb  23056  logdmss  23110  dvlog  23119  logbcl  23225  logbid1  23226  logb1  23227  elogb  23228  logbchbase  23229  relogbval  23230  relogbcl  23231  relogbreexp  23233  relogbmul  23235  nnlogbexp  23239  relogbcxp  23243  cxplogb  23244  relogbcxpb  23245  logbf  23247  logblog  23250  angval  23251  dcubic  23293  rlimcnp  23412  efrlim  23416  logexprlim  23617  dchrghm  23648  dchrabs  23652  lgsfcl2  23694  lgsval2lem  23698  lgsval3  23706  lgsmod  23713  lgsdirprm  23721  lgsne0  23725  lgsquad2lem2  23751  2sqlem11  23767  2sqblem  23769  dchrvmaeq0  23806  rpvmasum2  23814  dchrisum0re  23815  qrngdiv  23926  tglngval  24058  tgisline  24127  axlowdimlem9  24374  axlowdimlem12  24377  axlowdimlem13  24378  umgra1  24447  uslgra1  24493  cusgrarn  24580  cusgrafilem2  24601  sizeusglecusglem1  24605  nbhashuvtx  25037  umgrabi  25104  2pthfrgra  25132  3cyclfrgrarn1  25133  n4cyclfrgra  25139  ablomul  25474  mulid  25475  suppss3  27700  xdivval  27768  xrge0tsmsd  27929  ordtconlem1  28060  ispisys2  28302  sigapisys  28303  sibfinima  28464  sseqf  28514  signswch  28701  signstfvn  28709  signsvtn0  28710  signstfvcl  28713  signstfveq0a  28716  signstfveq0  28717  signsvfn  28722  signsvtp  28723  signsvtn  28724  signsvfpn  28725  signsvfnn  28726  signlem0  28727  subfacp1lem5  28817  cvmsi  28899  cvmsval  28900  cvmsdisj  28904  cvmscld  28907  cvmsss2  28908  sinccvglem  29227  circum  29229  itg2addnclem2  30233  sdclem1  30402  rrncmslem  30494  rrnequiv  30497  isdrngo2  30527  isdrngo3  30528  prtlem100  30762  prter2  30788  prter3  30789  pellexlem5  30934  dfac11  31174  dfacbasgrp  31225  dgraalem  31262  dgraaub  31265  aaitgo  31279  sdrgacs  31318  cntzsdrg  31319  proot1ex  31329  isdomn3  31332  deg1mhm  31335  ofdivrec  31399  ofdivcan4  31400  ofdivdiv2  31401  expgrowth  31408  binomcxplemnotnn0  31429  dvrecg  31873  dvmptdiv  31880  dvdivbd  31886  dvdivcncf  31890  dirkeritg  32050  fourierdlem39  32094  fourierdlem57  32112  fourierdlem58  32113  fourierdlem59  32114  fourierdlem68  32123  fourierdlem76  32131  fourierdlem103  32158  fourierdlem104  32159  fourierdlem111  32166  oddprmALTV  32529  elpwdifsn  32617  2zrngnmrid  32956  fdmdifeqresdif  33131  lincext1  33255  lindslinindsimp2lem5  33263  rege1logbrege0  33379  fllogbd  33381  relogbmulbexp  33382  relogbdivb  33383  nnpw2blen  33401  blennngt2o2  33413  blennn0e2  33415  dignn0ldlem  33423  aacllem  33550  bnj158  34131  bnj168  34132  bnj529  34145  bnj906  34335  bnj970  34352  lsatlspsn2  35130  lsateln0  35133  lsatn0  35137  lsatspn0  35138  lsatcmp  35141  lsatelbN  35144  islshpat  35155  lsat0cv  35171  lkrlspeqN  35309  dvheveccl  37252  dihlatat  37477  dochnel  37533  dihjat1  37569  dvh4dimlem  37583  dochsnkr2cl  37614  dochkr1  37618  dochkr1OLDN  37619  lcfl6lem  37638  lcfl9a  37645  lclkrlem2l  37658  lclkrlem2o  37661  lclkrlem2q  37663  lcfrlem9  37690  lcfrlem16  37698  lcfrlem17  37699  lcfrlem27  37709  lcfrlem37  37719  lcfrlem38  37720  lcfrlem40  37722  lcdlkreqN  37762  mapdrvallem2  37785  mapdn0  37809  mapdpglem20  37831  mapdpglem30  37842  mapdindp0  37859  mapdhcl  37867  mapdh6aN  37875  mapdh6dN  37879  mapdh6eN  37880  mapdh6kN  37886  mapdh8  37929  hdmap1l6a  37950  hdmap1l6d  37954  hdmap1l6e  37955  hdmap1l6k  37961  hdmapval3N  37981  hdmap10  37983  hdmap11lem2  37985  hdmapnzcl  37988  hdmaprnlem3eN  38001  hdmaprnlem17N  38006  hdmap14lem4a  38014  hdmap14lem7  38017  hdmap14lem14  38024  hgmaprnlem5N  38043  hdmaplkr  38056  hdmapip0  38058  hgmapvvlem2  38067  hgmapvvlem3  38068  hgmapvv  38069
  Copyright terms: Public domain W3C validator