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

Theorem eldifsn 4519
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 3790 . 2 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶}))
2 elsng 4395 . . . 4 (𝐴𝐵 → (𝐴 ∈ {𝐶} ↔ 𝐴 = 𝐶))
32necon3bbid 3026 . . 3 (𝐴𝐵 → (¬ 𝐴 ∈ {𝐶} ↔ 𝐴𝐶))
43pm5.32i 566 . 2 ((𝐴𝐵 ∧ ¬ 𝐴 ∈ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
51, 4bitri 266 1 (𝐴 ∈ (𝐵 ∖ {𝐶}) ↔ (𝐴𝐵𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 197  wa 384  wcel 2157  wne 2989  cdif 3777  {csn 4381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-v 3404  df-dif 3783  df-sn 4382
This theorem is referenced by:  ssdifsnOLD  4521  elpwdifsn  4522  eldifsni  4523  rexdifsn  4526  raldifsni  4527  eldifvsn  4529  difsn  4530  prproe  4639  sossfld  5804  tpres  6700  mpt2difsnif  6992  onmindif2  7251  mptsuppd  7561  suppssr  7570  suppssov1  7571  suppsssn  7574  suppssfv  7575  dif1o  7826  difsnen  8290  limenpsi  8383  frfi  8453  fofinf1o  8489  wemapso2lem  8705  en2eleq  9123  en2other2  9124  dfac8clem  9147  acni2  9161  acndom  9166  acnnum  9167  dfac9  9252  dfacacn  9257  kmlem3  9268  kmlem4  9269  fin23lem21  9455  canthp1lem2  9769  elni  9992  mulnzcnopr  10967  divval  10981  elnnne0  11592  elq  12028  rpcndif0  12084  modfzo0difsn  12985  modsumfzodifsn  12986  expcl2lem  13114  expclzlem  13126  hashdifpr  13439  prprrab  13491  hashle2prv  13496  reccn2  14569  rlimdiv  14618  eff2  15068  tanval  15097  rpnnen2lem9  15190  fzo0dvdseq  15287  oddprmgt2  15648  oddprmdvds  15843  4sqlem19  15903  prmlem0  16043  prmlem1a  16044  setsnid  16145  grpinvnzcl  17711  symgextf  18057  symgextfv  18058  f1omvdmvd  18083  pmtrprfv  18093  odcau  18239  efgsf  18362  efgsrel  18367  efgs1  18368  efgs1b  18369  efgsp1  18370  efgsres  18371  efgredlema  18373  efgredlemd  18377  efgrelexlemb  18383  gsumpt  18581  dmdprdd  18619  dprdcntz  18628  dprdfeq0  18642  dprd2da  18662  drngunit  18975  isdrng2  18980  drngid2  18986  isdrngd  18995  issubdrg  19028  abvtriv  19064  islss  19158  lssneln0  19176  lssneln0OLD  19177  lssssr  19178  lssssrOLD  19179  lbsind  19306  lbspss  19308  lspabs3  19347  lspsneq  19348  lspfixed  19354  lspfixedOLD  19355  lspexch  19356  islbs2  19382  isdomn2  19527  domnrrg  19528  mvrcl  19677  coe1tmmul2  19873  cnflddiv  20003  cnfldinv  20004  xrs1mnd  20011  xrs10  20012  xrge0subm  20014  cnsubdrglem  20024  cnmgpid  20035  cnmsubglem  20036  gzrngunit  20039  zringunit  20063  zringndrg  20065  domnchr  20107  cnmsgngrp  20151  psgninv  20154  psgndiflemB  20173  lindfind  20385  lindsind  20386  lindff1  20389  lindfrn  20390  mdetunilem9  20657  maducoeval2  20677  gsummatr01lem4  20696  ist1-2  21385  cmpfi  21445  2ndcdisj  21493  2ndcsep  21496  locfincmp  21563  alexsublem  22081  cldsubg  22147  imasdsf1olem  22411  prdsxmslem2  22567  reperflem  22854  xrge0gsumle  22869  xrge0tsms  22870  divcn  22904  evth  22991  cvsdiv  23164  cvsdivcl  23165  cphreccllem  23210  bcthlem5  23358  itg11  23694  i1fmullem  23697  i1fadd  23698  itg1addlem2  23700  i1fmulc  23706  itg1mulc  23707  ellimc3  23879  limcmpt2  23884  dvlem  23896  dvidlem  23915  dvcnp  23918  dvcobr  23945  dvrec  23954  dvrecg  23972  dvmptdiv  23973  dvcnvlem  23975  dvexp3  23977  dveflem  23978  dvferm1lem  23983  dvferm2lem  23985  lhop1lem  24012  ftc1lem5  24039  mdegleb  24060  coe1mul3  24095  ply1nz  24117  fta1blem  24164  fta1b  24165  ig1peu  24167  ig1pdvds  24172  plyeq0lem  24202  dgrub  24226  quotval  24283  fta1lem  24298  fta1  24299  elqaalem3  24312  qaa  24314  iaa  24316  aareccl  24317  aannenlem2  24320  abelthlem8  24429  abelth  24431  reefgim  24440  eff1olem  24531  logrncl  24550  eflog  24559  logeftb  24566  logdmss  24624  dvlog  24633  logbcl  24741  logbid1  24742  logb1  24743  elogb  24744  logbchbase  24745  relogbval  24746  relogbcl  24747  relogbreexp  24749  relogbmul  24751  nnlogbexp  24755  relogbcxp  24759  cxplogb  24760  relogbcxpb  24761  logbf  24763  logblog  24766  angval  24767  dcubic  24809  rlimcnp  24928  efrlim  24932  logexprlim  25186  dchrghm  25217  dchrabs  25221  lgsfcl2  25264  lgsval2lem  25268  lgsval3  25276  lgsmod  25284  lgsdirprm  25292  lgsne0  25296  gausslemma2dlem0f  25322  lgsquad2lem2  25346  2lgsoddprm  25377  2sqlem11  25390  2sqblem  25392  dchrvmaeq0  25429  rpvmasum2  25437  dchrisum0re  25438  qrngdiv  25549  tglngval  25682  tgisline  25758  axlowdimlem9  26066  axlowdimlem12  26069  axlowdimlem13  26070  upgrbi  26224  upgr1elem  26243  umgrislfupgrlem  26253  edgupgr  26265  subgruhgredgd  26414  upgrreslem  26434  nbgrel  26471  nbgrelOLD  26472  nbupgr  26478  nbupgrel  26479  nbumgrvtx  26480  nbgrssovtx  26495  nbgrssovtxOLD  26498  nbupgrres  26503  nbusgrvtxm1uvtx  26550  nbupgruvtxres  26552  iscplgredg  26563  cusgredg  26570  cusgrfilem2  26602  usgredgsscusgredg  26605  1loopgrnb0  26648  1egrvtxdg0  26657  uhgrvd00  26680  vtxdginducedm1lem4  26688  eupth2lem3lem3  27425  frcond1  27463  frcond4  27467  2pthfrgr  27481  3cyclfrgrrn1  27482  n4cyclfrgr  27488  frgrwopreglem4a  27507  numclwwlk5  27598  suppss3  29851  xdivval  29974  xrge0tsmsd  30132  submatminr1  30223  ordtconnlem1  30317  ispisys2  30563  sigapisys  30565  sibfinima  30748  sseqf  30801  signswch  30985  signstfvn  30993  signsvtn0  30994  signstfvcl  30997  signstfveq0a  31000  signstfveq0  31001  signsvfn  31006  signsvtp  31007  signsvtn  31008  signsvfpn  31009  signsvfnn  31010  signlem0  31011  bnj158  31142  bnj168  31143  bnj529  31155  bnj906  31344  bnj970  31361  subfacp1lem5  31510  cvmsi  31591  cvmsval  31592  cvmsdisj  31596  cvmscld  31599  cvmsss2  31600  sinccvglem  31909  circum  31911  unbdqndv2lem2  32839  bj-0int  33384  lindsenlbs  33735  matunitlindflem2  33737  matunitlindf  33738  poimirlem6  33746  poimirlem7  33747  poimirlem8  33748  poimirlem16  33756  poimirlem18  33758  poimirlem19  33759  poimirlem21  33761  poimirlem22  33762  poimirlem24  33764  poimirlem25  33765  poimirlem26  33766  poimirlem27  33767  itg2addnclem2  33792  sdclem1  33868  rrncmslem  33960  rrnequiv  33963  isdrngo2  34086  isdrngo3  34087  prtlem100  34656  prter2  34678  prter3  34679  lsatlspsn2  34790  lsateln0  34793  lsatn0  34797  lsatspn0  34798  lsatcmp  34801  lsatelbN  34804  islshpat  34815  lsat0cv  34831  lkrlspeqN  34969  dvheveccl  36910  dihlatat  37135  dochnel  37191  dihjat1  37227  dvh4dimlem  37241  dochsnkr2cl  37272  dochkr1  37276  dochkr1OLDN  37277  lcfl6lem  37296  lcfl9a  37303  lclkrlem2l  37316  lclkrlem2o  37319  lclkrlem2q  37321  lcfrlem9  37348  lcfrlem16  37356  lcfrlem17  37357  lcfrlem27  37367  lcfrlem37  37377  lcfrlem38  37378  lcfrlem40  37380  lcdlkreqN  37420  mapdrvallem2  37443  mapdn0  37467  mapdpglem20  37489  mapdpglem30  37500  mapdindp0  37517  mapdhcl  37525  mapdh6aN  37533  mapdh6dN  37537  mapdh6eN  37538  mapdh6kN  37544  mapdh8  37586  hdmap1l6a  37607  hdmap1l6d  37611  hdmap1l6e  37612  hdmap1l6k  37618  hdmapval3N  37636  hdmap10  37638  hdmap11lem2  37640  hdmapnzcl  37643  hdmaprnlem3eN  37656  hdmaprnlem17N  37661  hdmap14lem4a  37669  hdmap14lem7  37672  hdmap14lem14  37679  hgmaprnlem5N  37698  hdmaplkr  37711  hdmapip0  37713  hgmapvvlem2  37722  hgmapvvlem3  37723  hgmapvv  37724  pellexlem5  37916  dfac11  38150  dfacbasgrp  38196  dgraalem  38233  dgraaub  38236  aaitgo  38250  sdrgacs  38289  cntzsdrg  38290  proot1ex  38297  isdomn3  38300  deg1mhm  38303  ofdivrec  39042  ofdivcan4  39043  ofdivdiv2  39044  expgrowth  39051  binomcxplemnotnn0  39072  dvdivbd  40635  dvdivcncf  40639  dirkeritg  40815  fourierdlem39  40859  fourierdlem57  40876  fourierdlem58  40877  fourierdlem59  40878  fourierdlem68  40887  fourierdlem76  40895  fourierdlem103  40922  fourierdlem104  40923  fourierdlem111  40930  setsnidel  41939  odz2prm2pw  42067  fmtnoprmfac1  42069  fmtnoprmfac2  42071  sfprmdvdsmersenne  42112  lighneallem2  42115  lighneallem3  42116  lighneal  42120  oddprmALTV  42190  evenprm2  42215  oddprmne2  42216  odd2prm2  42219  even3prm2  42220  sprvalpwn0  42318  2zrngnmrid  42535  fdmdifeqresdif  42705  lincext1  42828  lindslinindsimp2lem5  42836  rege1logbrege0  42937  fllogbd  42939  relogbmulbexp  42940  relogbdivb  42941  nnpw2blen  42959  blennngt2o2  42971  blennn0e2  42973  dignn0ldlem  42981  aacllem  43135
  Copyright terms: Public domain W3C validator