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

Theorem eldifi 3931
Description: Implication of membership in a class difference. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
eldifi (𝐴 ∈ (𝐵𝐶) → 𝐴𝐵)

Proof of Theorem eldifi
StepHypRef Expression
1 eldif 3779 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
21simplbi 487 1 (𝐴 ∈ (𝐵𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2156  cdif 3766
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 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
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 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-dif 3772
This theorem is referenced by:  difss  3936  noel  4120  eqoreldif  4418  xpdifid  5773  tz7.7  5962  tfi  7283  peano5  7319  wfrlem10  7660  wfrlem15  7665  tz7.48-1  7774  tz7.49  7776  dif20el  7822  oaf1o  7880  oeordi  7904  oeord  7905  oecan  7906  oeword  7907  oeworde  7910  oelimcl  7917  oeeulem  7918  oeeui  7919  oaabs2  7962  boxcutc  8188  domdifsn  8282  isinf  8412  pssnn  8417  pwfilem  8499  fsuppco2  8547  fsuppcor  8548  ordtypelem7  8668  unxpwdom2  8732  inf3lem3  8774  cantnfp1lem1  8822  cantnfp1lem3  8824  infxpenc2lem1  9125  dfacacn  9248  isf32lem3  9462  isf34lem4  9484  fin67  9502  isfin7-2  9503  domtriomlem  9549  axdc2lem  9555  axdc3lem4  9560  axdc4lem  9562  ttukeylem7  9622  konigthlem  9675  fpwwe2lem13  9749  fpwwe2  9750  modfzo0difsn  12966  hashf1lem1  13456  hashle2prv  13477  rlimrege0  14533  rlimrecl  14534  sumrblem  14665  fsumcvg  14666  summolem2a  14669  fsumss  14679  fsumless  14750  cvgcmpce  14772  binomlem  14783  incexclem  14790  incexc  14791  isumltss  14802  prodrblem  14880  fprodcvg  14881  prodmolem2a  14885  fprodss  14899  fprodn0f  14942  fprodeq0g  14945  fprodmodd  14948  rpnnen2lem10  15172  rpnnen2lem11  15173  sumeven  15330  sumodd  15331  lcmfunsnlem2  15572  oddprmge3  15630  oddprm  15732  nnoddn2prm  15733  nnoddn2prmb  15735  iserodd  15757  prmreclem2  15838  prmreclem3  15839  prmreclem5  15841  4sqlem19  15884  prmdvdsprmo  15963  prmodvdslcmf  15968  prmlem0  16024  firest  16298  grpinvnzcl  17692  symgextfv  18039  pmtrf  18076  pmtrdifellem3  18099  sylow2alem2  18234  sylow2a  18235  efgsf  18343  efgsrel  18348  efgs1  18349  efgsfo  18353  efgredlemc  18359  gsumzaddlem  18522  gsumzadd  18523  gsumzmhm  18538  gsum2d2lem  18573  dprdfadd  18621  dprdres  18629  subgdmdprd  18635  dmdprdsplitlem  18638  dmdprdsplit2lem  18646  dpjidcl  18659  ablfac1b  18671  pgpfac1lem1  18675  gsummgp0  18810  isirred  18901  irredrmul  18909  isdrng2  18961  isdrngd  18976  lcomfsupp  19107  lbspropd  19306  lspsneq  19329  lsppratlem6  19361  lbsextlem2  19368  lbsextlem4  19370  ringelnzr  19475  psrbaglesupp  19577  psrlidm  19612  psrridm  19613  mplsubglem  19643  mpllsslem  19644  mplsubrglem  19648  mplmonmul  19673  mplcoe1  19674  mplcoe5  19677  mplbas2  19679  evlslem3  19722  coe1tmmul2  19854  coe1tmmul  19855  xrs1mnd  19992  xrs10  19993  xrs1cmn  19994  cnsubrg  20014  psgnodpm  20141  zrhpsgnodpm  20145  evpmodpmf1o  20150  uvcresum  20342  frlmssuvc1  20343  frlmsslsp  20345  frlmup2  20348  lindfrn  20370  f1lindf  20371  lindfmm  20376  islindf4  20387  dmatmul  20514  1marepvsma1  20600  mdetdiaglem  20615  mdetrlin  20619  mdetrsca  20620  mdetralt  20625  maducoeval2  20657  madugsum  20660  symgmatr01  20672  gsummatr01lem3  20675  gsummatr01lem4  20676  gsummatr01  20677  smadiadetlem0  20679  smadiadetlem1a  20681  cmpfi  21425  2ndcdisj2  21474  elptr2  21591  ptcnplem  21638  xkopt  21672  kqdisj  21749  fin1aufil  21949  ptcmplem2  22070  ptcmplem3  22071  ptcmplem4  22072  opnsubg  22124  lpbl  22521  blcld  22523  zcld  22829  recld2  22830  reconnlem1  22842  divcn  22884  iundisj  23529  mbfeqalem1  23622  itg1val2  23665  itg1ge0  23667  i1fmullem  23675  i1fadd  23676  itg1addlem4  23680  itg1mulc  23685  itg1lea  23693  itg1le  23694  mbfi1fseqlem4  23699  itg2uba  23724  itg2lea  23725  itg2eqa  23726  itg2splitlem  23729  itg2split  23730  itgeqa  23794  ellimc3  23857  dvaddbr  23915  dvmulbr  23916  dvcobr  23923  dvcjbr  23926  dvrec  23932  dvrecg  23950  dvcnvlem  23953  dvexp3  23955  dveflem  23956  tdeglem4  24034  deg1n0ima  24063  deg1mul3le  24090  ig1peu  24145  ply1termlem  24173  plypf1  24182  plyaddlem1  24183  plymullem1  24184  coeeulem  24194  coeidlem  24207  coeid3  24210  coefv0  24218  coemulhi  24224  coemulc  24225  dvply1  24253  fta1  24277  vieta1lem2  24280  elaa  24285  elqaalem2  24289  aannenlem2  24298  aaliou2  24309  tayl0  24330  dvtaylp  24338  taylthlem1  24341  taylthlem2  24342  pserdvlem2  24396  logbcl  24719  relogbreexp  24727  relogbcxp  24737  cxplogb  24738  dcubic  24787  rlimcnp  24906  jensen  24929  dmgmaddn0  24963  dmlogdmgm  24964  lgamgulmlem2  24970  igamz  24988  gamp1  24998  regamcl  25001  wilthlem2  25009  basellem3  25023  chpub  25159  logexprlim  25164  lgslem1  25236  lgslem4  25239  lgsvalmod  25255  lgsqr  25290  lgsqrmod  25291  lgsqrmodndvds  25292  gausslemma2dlem0b  25296  gausslemma2dlem0c  25297  gausslemma2dlem0i  25303  gausslemma2dlem1a  25304  gausslemma2dlem4  25308  gausslemma2dlem5a  25309  gausslemma2dlem7  25312  gausslemma2d  25313  lgsquadlem1  25319  lgsquad2  25325  m1lgs  25327  2lgsoddprm  25355  dchrisum0fno1  25414  rplogsum  25430  ishpg  25865  umgrislfupgrlem  26231  usgruspgrb  26291  nbumgrvtx  26458  nbupgrres  26481  isuvtx  26515  isuvtxaOLD  26516  cusgrexilem2  26566  cusgrexi  26567  structtocusgr  26570  cusgrres  26572  cusgrfilem2  26580  vtxdginducedm1  26667  cusconngr  27364  2pthfrgr  27459  frgrncvvdeq  27484  frgrwopreglem4  27490  frgrwopreglem5  27496  frgrwopreg  27498  frgrhash2wsp  27507  strlem1  29437  strlem3  29440  strlem4  29441  strlem5  29442  hstrlem3  29448  hstrlem4  29449  iundisjf  29727  suppss3  29829  iundisjfi  29882  qtophaus  30228  elzdif0  30349  ind0  30405  measvunilem  30600  sibfof  30727  eulerpartlemb  30755  eulerpartlemf  30757  sseqf  30779  ballotlem5  30886  ballotlemi1  30889  ballotlemii  30890  ballotlemic  30893  ballotlem1c  30894  ballotlemscr  30905  ballotlemro  30909  ballotlemfg  30912  ballotlemfrc  30913  ballotlemfrceq  30915  ballotlemrinv0  30919  plymulx0  30949  signstfvn  30971  bnj923  31161  bnj570  31298  bnj594  31305  subfacp1lem1  31484  mrsubcn  31739  mrsubco  31741  circum  31890  dfon2lem6  32013  neibastop1  32675  bj-restn0b  33355  lindsenlbs  33717  matunitlindflem1  33718  poimirlem24  33746  poimirlem25  33747  dvtan  33772  itg2addnclem2  33774  ftc1cnnc  33796  dvasin  33808  dvreasin  33810  dvreacos  33811  isdrngo2  34068  isdrngo3  34069  divrngidl  34138  isfldidl  34178  pridlc2  34182  pridlc3  34183  prter2  34660  lsateln0  34775  lsatlss  34776  lsmsat  34788  lsatcv0  34811  lsat0cv  34813  lcv1  34821  l1cvpat  34834  dih1dimatlem  37110  dihatexv2  37120  djhcvat42  37196  dihjat1lem  37209  dochsatshp  37232  lcfl6  37281  mapdrvallem2  37426  mapdpglem32  37486  irrapx1  37894  pell1234qrne0  37919  pell1234qrreccl  37920  pell1234qrmulcl  37921  pell14qrgt0  37925  pell1234qrdich  37927  pell14qrdich  37935  pell1qrge1  37936  pell1qr1  37937  pell1qrgap  37940  pell14qrgapw  37942  pellqrexplicit  37943  pellqrex  37945  pellfundge  37948  pellfundgt1  37949  setindtr  38092  kelac1  38134  mpaaeu  38221  flcidc  38245  cntzsdrg  38273  deg1mhm  38286  radcnvrat  39013  binomcxplemdvbinom  39052  disjiun2  39719  fiiuncl  39727  disjf1o  39867  difmapsn  39891  supminfxr2  40178  icoiccdif  40231  iccdificc  40246  fsumnncl  40283  fsumsplit1  40284  fsumsupp0  40290  fprod0  40308  climrec  40315  islpcn  40351  lptre2pt  40352  limclner  40363  cnrefiisplem  40535  fprodcncf  40594  fperdvper  40613  dvdivcncf  40622  dvnmul  40638  dvmptfprodlem  40639  dvnprodlem2  40642  stoweidlem25  40721  stoweidlem28  40724  stoweidlem41  40737  stoweidlem44  40740  stoweidlem46  40742  stirlinglem5  40774  dirkercncflem1  40799  dirkercncflem2  40800  fourierdlem24  40827  fourierdlem62  40864  fouriersw  40927  fouriercn  40928  elaa2lem  40929  elaa2  40930  etransclem25  40955  etransclem35  40965  etransclem44  40974  sge0iunmptlemfi  41109  sge0fodjrnlem  41112  iundjiunlem  41155  meadjiunlem  41161  meaiininclem  41182  isomenndlem  41226  hsphoidmvle2  41281  hsphoidmvle  41282  hoidmv1lelem2  41288  hoidmvle  41296  ovnhoilem1  41297  hspdifhsp  41312  hspmbllem2  41323  ovnsubadd2lem  41341  ovolval4lem1  41345  preimagelt  41394  preimalegt  41395  fsummsndifre  41917  fsummmodsndifre  41919  odz2prm2pw  42050  fmtnoprmfac1lem  42051  fmtnoprmfac2lem1  42053  2pwp1prm  42078  lighneallem2  42098  lighneallem3  42099  lighneallem4  42102  bgoldbtbndlem2  42269  bgoldbtbndlem3  42270  bgoldbtbndlem4  42271  bgoldbtbnd  42272  c0rhm  42480  c0rnghm  42481  zrrnghm  42485  2zrngnmlid2  42519  zrinitorngc  42568  zrtermorngc  42569  mgpsumunsn  42708  mgpsumz  42709  mgpsumn  42710  lindslinindsimp1  42814  lindslinindsimp2  42820  lincresunit1  42834  lincresunit2  42835  lincresunit3lem1  42836  lincresunit3lem2  42837  lincresunit3  42838  lindssnlvec  42843  logcxp0  42897  relogbmulbexp  42923  relogbdivb  42924  dignn0fr  42963
  Copyright terms: Public domain W3C validator