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

Theorem eldifi 3694
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 3550 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
21simplbi 475 1 (𝐴 ∈ (𝐵𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 1977  cdif 3537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543
This theorem is referenced by:  difss  3699  noel  3878  eqoreldif  4172  eqoreldifOLD  4173  xpdifid  5481  tz7.7  5666  tfi  6945  peano5  6981  wfrlem10  7311  wfrlem15  7316  tz7.48-1  7425  tz7.49  7427  dif20el  7472  oaf1o  7530  oeordi  7554  oeord  7555  oecan  7556  oeword  7557  oeworde  7560  oelimcl  7567  oeeulem  7568  oeeui  7569  oaabs2  7612  boxcutc  7837  domdifsn  7928  isinf  8058  pssnn  8063  pwfilem  8143  fsuppco2  8191  fsuppcor  8192  ordtypelem7  8312  unxpwdom2  8376  inf3lem3  8410  cantnfp1lem1  8458  cantnfp1lem3  8460  infxpenc2lem1  8725  dfacacn  8846  isf32lem3  9060  isf34lem4  9082  fin67  9100  isfin7-2  9101  domtriomlem  9147  axdc2lem  9153  axdc3lem4  9158  axdc4lem  9160  ttukeylem7  9220  konigthlem  9269  fpwwe2lem13  9343  fpwwe2  9344  modfzo0difsn  12604  hashf1lem1  13096  rlimrege0  14158  rlimrecl  14159  sumrblem  14289  fsumcvg  14290  summolem2a  14293  fsumss  14303  fsumless  14369  cvgcmpce  14391  binomlem  14400  incexclem  14407  incexc  14408  isumltss  14419  prodrblem  14498  fprodcvg  14499  prodmolem2a  14503  fprodss  14517  fprodn0f  14561  fprodeq0g  14564  fprodmodd  14567  rpnnen2lem10  14791  rpnnen2lem11  14792  sumeven  14948  sumodd  14949  lcmfunsnlem2  15191  oddprmge3  15250  oddprm  15353  nnoddn2prm  15354  nnoddn2prmb  15356  iserodd  15378  prmreclem2  15459  prmreclem3  15460  prmreclem5  15462  4sqlem19  15505  prmdvdsprmo  15584  prmodvdslcmf  15589  prmlem0  15650  firest  15916  grpinvnzcl  17310  symgextfv  17661  pmtrf  17698  pmtrdifellem3  17721  sylow2alem2  17856  sylow2a  17857  efgsf  17965  efgsrel  17970  efgs1  17971  efgsfo  17975  efgredlemc  17981  gsumzaddlem  18144  gsumzadd  18145  gsumzmhm  18160  gsum2d2lem  18195  dprdfadd  18242  dprdres  18250  subgdmdprd  18256  dmdprdsplitlem  18259  dmdprdsplit2lem  18267  dpjidcl  18280  ablfac1b  18292  pgpfac1lem1  18296  gsummgp0  18431  isirred  18522  irredrmul  18530  isdrng2  18580  isdrngd  18595  lcomfsupp  18726  lbspropd  18920  lspsneq  18943  lsppratlem6  18973  lbsextlem2  18980  lbsextlem4  18982  ringelnzr  19087  psrbaglesupp  19189  psrlidm  19224  psrridm  19225  mplsubglem  19255  mpllsslem  19256  mplsubrglem  19260  mplmonmul  19285  mplcoe1  19286  mplcoe5  19289  mplbas2  19291  evlslem3  19335  coe1tmmul2  19467  coe1tmmul  19468  xrs1mnd  19603  xrs10  19604  xrs1cmn  19605  cnsubrg  19625  psgnodpm  19753  zrhpsgnodpm  19757  evpmodpmf1o  19761  uvcresum  19951  frlmssuvc1  19952  frlmsslsp  19954  frlmup2  19957  lindfrn  19979  f1lindf  19980  lindfmm  19985  islindf4  19996  dmatmul  20122  1marepvsma1  20208  mdetdiaglem  20223  mdetrlin  20227  mdetrsca  20228  mdetralt  20233  maducoeval2  20265  madugsum  20268  symgmatr01  20279  gsummatr01lem3  20282  gsummatr01lem4  20283  gsummatr01  20284  smadiadetlem0  20286  smadiadetlem1a  20288  cmpfi  21021  2ndcdisj2  21070  elptr2  21187  ptcnplem  21234  xkopt  21268  kqdisj  21345  fin1aufil  21546  ptcmplem2  21667  ptcmplem3  21668  ptcmplem4  21669  opnsubg  21721  lpbl  22118  blcld  22120  zcld  22424  recld2  22425  reconnlem1  22437  divcn  22479  iundisj  23123  mbfeqalem  23215  itg1val2  23257  itg1ge0  23259  i1fmullem  23267  i1fadd  23268  itg1addlem4  23272  itg1mulc  23277  itg1lea  23285  itg1le  23286  mbfi1fseqlem4  23291  itg2uba  23316  itg2lea  23317  itg2eqa  23318  itg2splitlem  23321  itg2split  23322  itgeqa  23386  ellimc3  23449  dvaddbr  23507  dvmulbr  23508  dvcobr  23515  dvcjbr  23518  dvrec  23524  dvcnvlem  23543  dvexp3  23545  dveflem  23546  tdeglem4  23624  deg1n0ima  23653  deg1mul3le  23680  ig1peu  23735  ply1termlem  23763  plypf1  23772  plyaddlem1  23773  plymullem1  23774  coeeulem  23784  coeidlem  23797  coeid3  23800  coefv0  23808  coemulhi  23814  coemulc  23815  dvply1  23843  fta1  23867  vieta1lem2  23870  elaa  23875  elqaalem2  23879  aannenlem2  23888  aaliou2  23899  tayl0  23920  dvtaylp  23928  taylthlem1  23931  taylthlem2  23932  pserdvlem2  23986  logbcl  24305  relogbreexp  24313  relogbcxp  24323  cxplogb  24324  dcubic  24373  rlimcnp  24492  jensen  24515  dmgmaddn0  24549  dmlogdmgm  24550  lgamgulmlem2  24556  igamz  24574  gamp1  24584  regamcl  24587  wilthlem2  24595  basellem3  24609  chpub  24745  logexprlim  24750  lgslem1  24822  lgslem4  24825  lgsvalmod  24841  lgsqr  24876  lgsqrmod  24877  lgsqrmodndvds  24878  gausslemma2dlem0b  24882  gausslemma2dlem0c  24883  gausslemma2dlem0i  24889  gausslemma2dlem1a  24890  gausslemma2dlem4  24894  gausslemma2dlem5a  24895  gausslemma2dlem7  24898  gausslemma2d  24899  lgsquadlem1  24905  lgsquad2  24911  m1lgs  24913  2lgsoddprm  24941  dchrisum0fno1  25000  rplogsum  25016  ishpg  25451  umgrislfupgrlem  25788  cusgraexi  25997  uvtxnbgra  26021  cusconngra  26204  frgrancvvdeqlem9  26568  frgrancvvdeq  26569  frgrancvvdgeq  26570  2spotiundisj  26589  frghash2spot  26590  strlem1  28493  strlem3  28496  strlem4  28497  strlem5  28498  hstrlem3  28504  hstrlem4  28505  iundisjf  28784  suppss3  28890  iundisjfi  28942  qtophaus  29231  elzdif0  29352  ind0  29409  measvunilem  29602  sibfof  29729  eulerpartlemb  29757  eulerpartlemf  29759  sseqf  29781  ballotlem5  29888  ballotlemi1  29891  ballotlemii  29892  ballotlemic  29895  ballotlem1c  29896  ballotlemscr  29907  ballotlemro  29911  ballotlemfg  29914  ballotlemfrc  29915  ballotlemfrceq  29917  ballotlemrinv0  29921  plymulx0  29950  signstfvn  29972  bnj923  30092  bnj570  30229  bnj594  30236  subfacp1lem1  30415  mrsubcn  30670  mrsubco  30672  circum  30822  dfon2lem6  30937  neibastop1  31524  bj-restn0b  32225  lindsenlbs  32574  matunitlindflem1  32575  poimirlem24  32603  poimirlem25  32604  dvtan  32630  itg2addnclem2  32632  ftc1cnnc  32654  dvasin  32666  dvreasin  32668  dvreacos  32669  isdrngo2  32927  isdrngo3  32928  divrngidl  32997  isfldidl  33037  pridlc2  33041  pridlc3  33042  prter2  33184  lsateln0  33300  lsatlss  33301  lsmsat  33313  lsatcv0  33336  lsat0cv  33338  lcv1  33346  l1cvpat  33359  dih1dimatlem  35636  dihatexv2  35646  djhcvat42  35722  dihjat1lem  35735  dochsatshp  35758  lcfl6  35807  mapdrvallem2  35952  mapdpglem32  36012  irrapx1  36410  pell1234qrne0  36435  pell1234qrreccl  36436  pell1234qrmulcl  36437  pell14qrgt0  36441  pell1234qrdich  36443  pell14qrdich  36451  pell1qrge1  36452  pell1qr1  36453  pell1qrgap  36456  pell14qrgapw  36458  pellqrexplicit  36459  pellqrex  36461  pellfundge  36464  pellfundgt1  36465  setindtr  36609  kelac1  36651  mpaaeu  36739  flcidc  36763  cntzsdrg  36791  deg1mhm  36804  radcnvrat  37535  binomcxplemdvbinom  37574  disjiun2  38251  fiiuncl  38259  disjf1o  38373  difmapsn  38399  icoiccdif  38597  iccdificc  38613  fsumnncl  38638  fsumsplit1  38639  fsumsupp0  38645  fprod0  38663  climrec  38670  islpcn  38706  lptre2pt  38707  limclner  38718  fprodcncf  38787  dvrecg  38800  fperdvper  38808  dvdivcncf  38817  dvnmul  38833  dvmptfprodlem  38834  dvnprodlem2  38837  stoweidlem25  38918  stoweidlem28  38921  stoweidlem41  38934  stoweidlem44  38937  stoweidlem46  38939  stirlinglem5  38971  dirkercncflem1  38996  dirkercncflem2  38997  fourierdlem24  39024  fourierdlem62  39061  fouriersw  39124  fouriercn  39125  elaa2lem  39126  elaa2  39127  etransclem25  39152  etransclem35  39162  etransclem44  39171  sge0iunmptlemfi  39306  sge0fodjrnlem  39309  iundjiunlem  39352  meadjiunlem  39358  meaiininclem  39376  isomenndlem  39420  hsphoidmvle2  39475  hsphoidmvle  39476  hoidmv1lelem2  39482  hoidmvle  39490  ovnhoilem1  39491  hspdifhsp  39506  hspmbllem2  39517  ovnsubadd2lem  39535  ovolval4lem1  39539  preimagelt  39589  preimalegt  39590  odz2prm2pw  40013  fmtnoprmfac1lem  40014  fmtnoprmfac2lem1  40016  2pwp1prm  40041  lighneallem2  40061  lighneallem3  40062  lighneallem4  40065  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  bgoldbtbndlem4  40224  bgoldbtbnd  40225  fsummsndifre  40371  fsummmodsndifre  40373  usgruspgrb  40411  nbumgrvtx  40568  nbupgrres  40592  isuvtxa  40621  cusgrexi  40662  cusgrres  40664  cusgrfilem2  40672  cusconngr  41358  2pthfrgr  41454  frgrncvvdeq  41480  frgrhash2wsp  41497  c0rhm  41702  c0rnghm  41703  zrrnghm  41707  2zrngnmlid2  41741  zrinitorngc  41792  zrtermorngc  41793  mgpsumunsn  41933  mgpsumz  41934  mgpsumn  41935  lindslinindsimp1  42040  lindslinindsimp2  42046  lincresunit1  42060  lincresunit2  42061  lincresunit3lem1  42062  lincresunit3lem2  42063  lincresunit3  42064  lindssnlvec  42069  logcxp0  42127  relogbmulbexp  42153  relogbdivb  42154  dignn0fr  42193
  Copyright terms: Public domain W3C validator