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

Theorem eldifi 3765
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 3617 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
21simplbi 475 1 (𝐴 ∈ (𝐵𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2030  cdif 3604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610
This theorem is referenced by:  difss  3770  noel  3952  eqoreldif  4257  eqoreldifOLD  4258  xpdifid  5597  tz7.7  5787  tfi  7095  peano5  7131  wfrlem10  7469  wfrlem15  7474  tz7.48-1  7583  tz7.49  7585  dif20el  7630  oaf1o  7688  oeordi  7712  oeord  7713  oecan  7714  oeword  7715  oeworde  7718  oelimcl  7725  oeeulem  7726  oeeui  7727  oaabs2  7770  boxcutc  7993  domdifsn  8084  isinf  8214  pssnn  8219  pwfilem  8301  fsuppco2  8349  fsuppcor  8350  ordtypelem7  8470  unxpwdom2  8534  inf3lem3  8565  cantnfp1lem1  8613  cantnfp1lem3  8615  infxpenc2lem1  8880  dfacacn  9001  isf32lem3  9215  isf34lem4  9237  fin67  9255  isfin7-2  9256  domtriomlem  9302  axdc2lem  9308  axdc3lem4  9313  axdc4lem  9315  ttukeylem7  9375  konigthlem  9428  fpwwe2lem13  9502  fpwwe2  9503  modfzo0difsn  12782  hashf1lem1  13277  hashle2prv  13298  rlimrege0  14354  rlimrecl  14355  sumrblem  14486  fsumcvg  14487  summolem2a  14490  fsumss  14500  fsumless  14572  cvgcmpce  14594  binomlem  14605  incexclem  14612  incexc  14613  isumltss  14624  prodrblem  14703  fprodcvg  14704  prodmolem2a  14708  fprodss  14722  fprodn0f  14766  fprodeq0g  14769  fprodmodd  14772  rpnnen2lem10  14996  rpnnen2lem11  14997  sumeven  15157  sumodd  15158  lcmfunsnlem2  15400  oddprmge3  15459  oddprm  15562  nnoddn2prm  15563  nnoddn2prmb  15565  iserodd  15587  prmreclem2  15668  prmreclem3  15669  prmreclem5  15671  4sqlem19  15714  prmdvdsprmo  15793  prmodvdslcmf  15798  prmlem0  15859  firest  16140  grpinvnzcl  17534  symgextfv  17884  pmtrf  17921  pmtrdifellem3  17944  sylow2alem2  18079  sylow2a  18080  efgsf  18188  efgsrel  18193  efgs1  18194  efgsfo  18198  efgredlemc  18204  gsumzaddlem  18367  gsumzadd  18368  gsumzmhm  18383  gsum2d2lem  18418  dprdfadd  18465  dprdres  18473  subgdmdprd  18479  dmdprdsplitlem  18482  dmdprdsplit2lem  18490  dpjidcl  18503  ablfac1b  18515  pgpfac1lem1  18519  gsummgp0  18654  isirred  18745  irredrmul  18753  isdrng2  18805  isdrngd  18820  lcomfsupp  18951  lbspropd  19147  lspsneq  19170  lsppratlem6  19200  lbsextlem2  19207  lbsextlem4  19209  ringelnzr  19314  psrbaglesupp  19416  psrlidm  19451  psrridm  19452  mplsubglem  19482  mpllsslem  19483  mplsubrglem  19487  mplmonmul  19512  mplcoe1  19513  mplcoe5  19516  mplbas2  19518  evlslem3  19562  coe1tmmul2  19694  coe1tmmul  19695  xrs1mnd  19832  xrs10  19833  xrs1cmn  19834  cnsubrg  19854  psgnodpm  19982  zrhpsgnodpm  19986  evpmodpmf1o  19990  uvcresum  20180  frlmssuvc1  20181  frlmsslsp  20183  frlmup2  20186  lindfrn  20208  f1lindf  20209  lindfmm  20214  islindf4  20225  dmatmul  20351  1marepvsma1  20437  mdetdiaglem  20452  mdetrlin  20456  mdetrsca  20457  mdetralt  20462  maducoeval2  20494  madugsum  20497  symgmatr01  20508  gsummatr01lem3  20511  gsummatr01lem4  20512  gsummatr01  20513  smadiadetlem0  20515  smadiadetlem1a  20517  cmpfi  21259  2ndcdisj2  21308  elptr2  21425  ptcnplem  21472  xkopt  21506  kqdisj  21583  fin1aufil  21783  ptcmplem2  21904  ptcmplem3  21905  ptcmplem4  21906  opnsubg  21958  lpbl  22355  blcld  22357  zcld  22663  recld2  22664  reconnlem1  22676  divcn  22718  iundisj  23362  mbfeqalem  23454  itg1val2  23496  itg1ge0  23498  i1fmullem  23506  i1fadd  23507  itg1addlem4  23511  itg1mulc  23516  itg1lea  23524  itg1le  23525  mbfi1fseqlem4  23530  itg2uba  23555  itg2lea  23556  itg2eqa  23557  itg2splitlem  23560  itg2split  23561  itgeqa  23625  ellimc3  23688  dvaddbr  23746  dvmulbr  23747  dvcobr  23754  dvcjbr  23757  dvrec  23763  dvrecg  23781  dvcnvlem  23784  dvexp3  23786  dveflem  23787  tdeglem4  23865  deg1n0ima  23894  deg1mul3le  23921  ig1peu  23976  ply1termlem  24004  plypf1  24013  plyaddlem1  24014  plymullem1  24015  coeeulem  24025  coeidlem  24038  coeid3  24041  coefv0  24049  coemulhi  24055  coemulc  24056  dvply1  24084  fta1  24108  vieta1lem2  24111  elaa  24116  elqaalem2  24120  aannenlem2  24129  aaliou2  24140  tayl0  24161  dvtaylp  24169  taylthlem1  24172  taylthlem2  24173  pserdvlem2  24227  logbcl  24550  relogbreexp  24558  relogbcxp  24568  cxplogb  24569  dcubic  24618  rlimcnp  24737  jensen  24760  dmgmaddn0  24794  dmlogdmgm  24795  lgamgulmlem2  24801  igamz  24819  gamp1  24829  regamcl  24832  wilthlem2  24840  basellem3  24854  chpub  24990  logexprlim  24995  lgslem1  25067  lgslem4  25070  lgsvalmod  25086  lgsqr  25121  lgsqrmod  25122  lgsqrmodndvds  25123  gausslemma2dlem0b  25127  gausslemma2dlem0c  25128  gausslemma2dlem0i  25134  gausslemma2dlem1a  25135  gausslemma2dlem4  25139  gausslemma2dlem5a  25140  gausslemma2dlem7  25143  gausslemma2d  25144  lgsquadlem1  25150  lgsquad2  25156  m1lgs  25158  2lgsoddprm  25186  dchrisum0fno1  25245  rplogsum  25261  ishpg  25696  umgrislfupgrlem  26062  usgruspgrb  26121  nbumgrvtx  26287  nbupgrres  26310  isuvtx  26343  isuvtxaOLD  26344  cusgrexilem2  26394  cusgrexi  26395  structtocusgr  26398  cusgrres  26400  cusgrfilem2  26408  vtxdginducedm1  26495  cusconngr  27169  2pthfrgr  27264  frgrncvvdeq  27289  frgrwopreglem4  27295  frgrwopreglem5  27301  frgrwopreg  27303  frgrhash2wsp  27312  strlem1  29237  strlem3  29240  strlem4  29241  strlem5  29242  hstrlem3  29248  hstrlem4  29249  iundisjf  29528  suppss3  29630  iundisjfi  29683  qtophaus  30031  elzdif0  30152  ind0  30208  measvunilem  30403  sibfof  30530  eulerpartlemb  30558  eulerpartlemf  30560  sseqf  30582  ballotlem5  30689  ballotlemi1  30692  ballotlemii  30693  ballotlemic  30696  ballotlem1c  30697  ballotlemscr  30708  ballotlemro  30712  ballotlemfg  30715  ballotlemfrc  30716  ballotlemfrceq  30718  ballotlemrinv0  30722  plymulx0  30752  signstfvn  30774  bnj923  30964  bnj570  31101  bnj594  31108  subfacp1lem1  31287  mrsubcn  31542  mrsubco  31544  circum  31694  dfon2lem6  31817  neibastop1  32479  bj-restn0b  33169  lindsenlbs  33534  matunitlindflem1  33535  poimirlem24  33563  poimirlem25  33564  dvtan  33590  itg2addnclem2  33592  ftc1cnnc  33614  dvasin  33626  dvreasin  33628  dvreacos  33629  isdrngo2  33887  isdrngo3  33888  divrngidl  33957  isfldidl  33997  pridlc2  34001  pridlc3  34002  prter2  34485  lsateln0  34600  lsatlss  34601  lsmsat  34613  lsatcv0  34636  lsat0cv  34638  lcv1  34646  l1cvpat  34659  dih1dimatlem  36935  dihatexv2  36945  djhcvat42  37021  dihjat1lem  37034  dochsatshp  37057  lcfl6  37106  mapdrvallem2  37251  mapdpglem32  37311  irrapx1  37709  pell1234qrne0  37734  pell1234qrreccl  37735  pell1234qrmulcl  37736  pell14qrgt0  37740  pell1234qrdich  37742  pell14qrdich  37750  pell1qrge1  37751  pell1qr1  37752  pell1qrgap  37755  pell14qrgapw  37757  pellqrexplicit  37758  pellqrex  37760  pellfundge  37763  pellfundgt1  37764  setindtr  37908  kelac1  37950  mpaaeu  38037  flcidc  38061  cntzsdrg  38089  deg1mhm  38102  radcnvrat  38830  binomcxplemdvbinom  38869  disjiun2  39540  fiiuncl  39548  disjf1o  39692  difmapsn  39718  supminfxr2  40012  icoiccdif  40068  iccdificc  40084  fsumnncl  40121  fsumsplit1  40122  fsumsupp0  40128  fprod0  40146  climrec  40153  islpcn  40189  lptre2pt  40190  limclner  40201  cnrefiisplem  40373  fprodcncf  40432  fperdvper  40451  dvdivcncf  40460  dvnmul  40476  dvmptfprodlem  40477  dvnprodlem2  40480  stoweidlem25  40560  stoweidlem28  40563  stoweidlem41  40576  stoweidlem44  40579  stoweidlem46  40581  stirlinglem5  40613  dirkercncflem1  40638  dirkercncflem2  40639  fourierdlem24  40666  fourierdlem62  40703  fouriersw  40766  fouriercn  40767  elaa2lem  40768  elaa2  40769  etransclem25  40794  etransclem35  40804  etransclem44  40813  sge0iunmptlemfi  40948  sge0fodjrnlem  40951  iundjiunlem  40994  meadjiunlem  41000  meaiininclem  41021  isomenndlem  41065  hsphoidmvle2  41120  hsphoidmvle  41121  hoidmv1lelem2  41127  hoidmvle  41135  ovnhoilem1  41136  hspdifhsp  41151  hspmbllem2  41162  ovnsubadd2lem  41180  ovolval4lem1  41184  preimagelt  41233  preimalegt  41234  fsummsndifre  41667  fsummmodsndifre  41669  odz2prm2pw  41800  fmtnoprmfac1lem  41801  fmtnoprmfac2lem1  41803  2pwp1prm  41828  lighneallem2  41848  lighneallem3  41849  lighneallem4  41852  bgoldbtbndlem2  42019  bgoldbtbndlem3  42020  bgoldbtbndlem4  42021  bgoldbtbnd  42022  c0rhm  42237  c0rnghm  42238  zrrnghm  42242  2zrngnmlid2  42276  zrinitorngc  42325  zrtermorngc  42326  mgpsumunsn  42465  mgpsumz  42466  mgpsumn  42467  lindslinindsimp1  42571  lindslinindsimp2  42577  lincresunit1  42591  lincresunit2  42592  lincresunit3lem1  42593  lincresunit3lem2  42594  lincresunit3  42595  lindssnlvec  42600  logcxp0  42654  relogbmulbexp  42680  relogbdivb  42681  dignn0fr  42720
  Copyright terms: Public domain W3C validator