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

Theorem eldifsn 4294
Description: Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007.)
Assertion
Ref Expression
eldifsn (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))

Proof of Theorem eldifsn
StepHypRef Expression
1 eldif 3570 . 2 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2 elsng 4169 . . . 4 (𝐴𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
32necon3bbid 2827 . . 3 (𝐴𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴𝐶))
43pm5.32i 668 . 2 ((𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
51, 4bitri 264 1 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wa 384  wcel 1987  wne 2790  cdif 3557  {csn 4155
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-v 3192  df-dif 3563  df-sn 4156
This theorem is referenced by:  elpwdifsn  4295  eldifsni  4296  rexdifsn  4299  raldifsni  4300  eldifvsn  4302  difsn  4304  sossfld  5549  tpres  6431  mpt2difsnif  6718  onmindif2  6974  mptsuppd  7278  suppssr  7286  suppssov1  7287  suppsssn  7290  suppssfv  7291  dif1o  7540  difsnen  8002  limenpsi  8095  frfi  8165  fofinf1o  8201  wemapso2lem  8417  en2eleq  8791  en2other2  8792  dfac8clem  8815  acni2  8829  acndom  8834  acnnum  8835  dfac9  8918  dfacacn  8923  kmlem3  8934  kmlem4  8935  fin23lem21  9121  canthp1lem2  9435  elni  9658  mulnzcnopr  10633  divval  10647  elnnne0  11266  elq  11750  rpcndif0  11811  modfzo0difsn  12698  modsumfzodifsn  12699  expcl2lem  12828  expclzlem  12840  hashdifpr  13159  prprrab  13209  hashle2prv  13214  reccn2  14277  rlimdiv  14326  eff2  14773  tanval  14802  rpnnen2lem9  14895  fzo0dvdseq  14988  oddprmgt2  15354  prmn2uzge3OLD  15356  oddprmdvds  15550  4sqlem19  15610  prmlem0  15755  prmlem1a  15756  setsnid  15855  grpinvnzcl  17427  symgextf  17777  symgextfv  17778  f1omvdmvd  17803  pmtrprfv  17813  odcau  17959  efgsf  18082  efgsrel  18087  efgs1  18088  efgs1b  18089  efgsp1  18090  efgsres  18091  efgredlema  18093  efgredlemd  18097  efgrelexlemb  18103  gsumpt  18301  dmdprdd  18338  dprdcntz  18347  dprdfeq0  18361  dprd2da  18381  drngunit  18692  isdrng2  18697  drngid2  18703  isdrngd  18712  issubdrg  18745  abvtriv  18781  islss  18875  lssneln0  18892  lssssr  18893  lbsind  19020  lbspss  19022  lspabs3  19061  lspsneq  19062  lspfixed  19068  lspexch  19069  islbs2  19094  isdomn2  19239  domnrrg  19240  mvrcl  19389  coe1tmmul2  19586  cnflddiv  19716  cnfldinv  19717  xrs1mnd  19724  xrs10  19725  xrge0subm  19727  cnsubdrglem  19737  cnmgpid  19748  cnmsubglem  19749  gzrngunit  19752  zringunit  19776  zringndrg  19778  domnchr  19820  cnmsgngrp  19865  psgninv  19868  psgndiflemB  19886  lindfind  20095  lindsind  20096  lindff1  20099  lindfrn  20100  mdetunilem9  20366  maducoeval2  20386  gsummatr01lem4  20404  ist1-2  21091  cmpfi  21151  2ndcdisj  21199  2ndcsep  21202  locfincmp  21269  alexsublem  21788  cldsubg  21854  imasdsf1olem  22118  prdsxmslem2  22274  reperflem  22561  xrge0gsumle  22576  xrge0tsms  22577  divcn  22611  evth  22698  cvsdiv  22872  cvsdivcl  22873  cphreccllem  22918  bcthlem5  23065  itg11  23398  i1fmullem  23401  i1fadd  23402  itg1addlem2  23404  i1fmulc  23410  itg1mulc  23411  ellimc3  23583  limcmpt2  23588  dvlem  23600  dvidlem  23619  dvcnp  23622  dvcobr  23649  dvrec  23658  dvcnvlem  23677  dvexp3  23679  dveflem  23680  dvferm1lem  23685  dvferm2lem  23687  lhop1lem  23714  ftc1lem5  23741  mdegleb  23762  coe1mul3  23797  ply1nz  23819  fta1blem  23866  fta1b  23867  ig1peu  23869  ig1pdvds  23874  plyeq0lem  23904  dgrub  23928  quotval  23985  fta1lem  24000  fta1  24001  elqaalem3  24014  qaa  24016  iaa  24018  aareccl  24019  aannenlem2  24022  abelthlem8  24131  abelth  24133  reefgim  24142  eff1olem  24232  logrncl  24252  eflog  24261  logeftb  24268  logdmss  24322  dvlog  24331  logbcl  24439  logbid1  24440  logb1  24441  elogb  24442  logbchbase  24443  relogbval  24444  relogbcl  24445  relogbreexp  24447  relogbmul  24449  nnlogbexp  24453  relogbcxp  24457  cxplogb  24458  relogbcxpb  24459  logbf  24461  logblog  24464  angval  24465  dcubic  24507  rlimcnp  24626  efrlim  24630  logexprlim  24884  dchrghm  24915  dchrabs  24919  lgsfcl2  24962  lgsval2lem  24966  lgsval3  24974  lgsmod  24982  lgsdirprm  24990  lgsne0  24994  gausslemma2dlem0f  25020  lgsquad2lem2  25044  2lgsoddprm  25075  2sqlem11  25088  2sqblem  25090  dchrvmaeq0  25127  rpvmasum2  25135  dchrisum0re  25136  qrngdiv  25247  tglngval  25380  tgisline  25456  axlowdimlem9  25764  axlowdimlem12  25767  axlowdimlem13  25768  upgrbi  25918  upgr1elem  25936  umgrislfupgrlem  25946  edgupgr  25958  subgruhgredgd  26103  nbgrel  26159  nbupgr  26161  nbupgrel  26162  nbumgrvtx  26163  nbgrssovtx  26181  nbupgrres  26187  nbusgrvtxm1uvtx  26227  nbupgruvtxres  26229  iscplgredg  26234  cusgredg  26241  cusgrfilem2  26273  usgredgsscusgredg  26276  1loopgrnb0  26318  1egrvtxdg0  26327  uhgrvd00  26350  eupth2lem3lem3  26990  frcond1  27030  2pthfrgr  27046  3cyclfrgrrn1  27047  n4cyclfrgr  27053  numclwwlk5  27134  suppss3  29386  xdivval  29454  xrge0tsmsd  29612  submatminr1  29700  ordtconnlem1  29794  ispisys2  30039  sigapisys  30041  sibfinima  30224  sseqf  30277  signswch  30460  signstfvn  30468  signsvtn0  30469  signstfvcl  30472  signstfveq0a  30475  signstfveq0  30476  signsvfn  30481  signsvtp  30482  signsvtn  30483  signsvfpn  30484  signsvfnn  30485  signlem0  30486  itgexpif  30493  bnj158  30558  bnj168  30559  bnj529  30572  bnj906  30761  bnj970  30778  subfacp1lem5  30927  cvmsi  31008  cvmsval  31009  cvmsdisj  31013  cvmscld  31016  cvmsss2  31017  sinccvglem  31327  circum  31329  unbdqndv2lem2  32196  lindsenlbs  33075  matunitlindflem2  33077  matunitlindf  33078  poimirlem6  33086  poimirlem7  33087  poimirlem8  33088  poimirlem16  33096  poimirlem18  33098  poimirlem19  33099  poimirlem21  33101  poimirlem22  33102  poimirlem24  33104  poimirlem25  33105  poimirlem26  33106  poimirlem27  33107  itg2addnclem2  33133  sdclem1  33210  rrncmslem  33302  rrnequiv  33305  isdrngo2  33428  isdrngo3  33429  prtlem100  33662  prter2  33685  prter3  33686  lsatlspsn2  33798  lsateln0  33801  lsatn0  33805  lsatspn0  33806  lsatcmp  33809  lsatelbN  33812  islshpat  33823  lsat0cv  33839  lkrlspeqN  33977  dvheveccl  35920  dihlatat  36145  dochnel  36201  dihjat1  36237  dvh4dimlem  36251  dochsnkr2cl  36282  dochkr1  36286  dochkr1OLDN  36287  lcfl6lem  36306  lcfl9a  36313  lclkrlem2l  36326  lclkrlem2o  36329  lclkrlem2q  36331  lcfrlem9  36358  lcfrlem16  36366  lcfrlem17  36367  lcfrlem27  36377  lcfrlem37  36387  lcfrlem38  36388  lcfrlem40  36390  lcdlkreqN  36430  mapdrvallem2  36453  mapdn0  36477  mapdpglem20  36499  mapdpglem30  36510  mapdindp0  36527  mapdhcl  36535  mapdh6aN  36543  mapdh6dN  36547  mapdh6eN  36548  mapdh6kN  36554  mapdh8  36597  hdmap1l6a  36618  hdmap1l6d  36622  hdmap1l6e  36623  hdmap1l6k  36629  hdmapval3N  36649  hdmap10  36651  hdmap11lem2  36653  hdmapnzcl  36656  hdmaprnlem3eN  36669  hdmaprnlem17N  36674  hdmap14lem4a  36682  hdmap14lem7  36685  hdmap14lem14  36692  hgmaprnlem5N  36711  hdmaplkr  36724  hdmapip0  36726  hgmapvvlem2  36735  hgmapvvlem3  36736  hgmapvv  36737  pellexlem5  36916  dfac11  37151  dfacbasgrp  37198  dgraalem  37235  dgraaub  37238  aaitgo  37252  sdrgacs  37291  cntzsdrg  37292  proot1ex  37299  isdomn3  37302  deg1mhm  37305  ofdivrec  38046  ofdivcan4  38047  ofdivdiv2  38048  expgrowth  38055  binomcxplemnotnn0  38076  dvrecg  39462  dvmptdiv  39469  dvdivbd  39475  dvdivcncf  39479  dirkeritg  39656  fourierdlem39  39700  fourierdlem57  39717  fourierdlem58  39718  fourierdlem59  39719  fourierdlem68  39728  fourierdlem76  39736  fourierdlem103  39763  fourierdlem104  39764  fourierdlem111  39771  setsnidel  40675  odz2prm2pw  40804  fmtnoprmfac1  40806  fmtnoprmfac2  40808  sfprmdvdsmersenne  40849  lighneallem2  40852  lighneallem3  40853  lighneal  40857  oddprmALTV  40927  evenprm2  40952  oddprmne2  40953  sprvalpwn0  41051  2zrngnmrid  41268  fdmdifeqresdif  41438  lincext1  41561  lindslinindsimp2lem5  41569  rege1logbrege0  41674  fllogbd  41676  relogbmulbexp  41677  relogbdivb  41678  nnpw2blen  41696  blennngt2o2  41708  blennn0e2  41710  dignn0ldlem  41718  ssdifsn  41752  aacllem  41880
  Copyright terms: Public domain W3C validator