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

Theorem eldifi 3693
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 3549 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
21simplbi 474 1 (𝐴 ∈ (𝐵𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 1976  cdif 3536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-dif 3542
This theorem is referenced by:  difss  3698  noel  3877  eqoreldif  4171  eqoreldifOLD  4172  xpdifid  5467  tz7.7  5652  tfi  6923  peano5  6959  wfrlem10  7289  wfrlem15  7294  tz7.48-1  7403  tz7.49  7405  dif20el  7450  oaf1o  7508  oeordi  7532  oeord  7533  oecan  7534  oeword  7535  oeworde  7538  oelimcl  7545  oeeulem  7546  oeeui  7547  oaabs2  7590  boxcutc  7815  domdifsn  7906  isinf  8036  pssnn  8041  pwfilem  8121  fsuppco2  8169  fsuppcor  8170  ordtypelem7  8290  unxpwdom2  8354  inf3lem3  8388  cantnfp1lem1  8436  cantnfp1lem3  8438  infxpenc2lem1  8703  dfacacn  8824  isf32lem3  9038  isf34lem4  9060  fin67  9078  isfin7-2  9079  domtriomlem  9125  axdc2lem  9131  axdc3lem4  9136  axdc4lem  9138  ttukeylem7  9198  konigthlem  9247  fpwwe2lem13  9321  fpwwe2  9322  modfzo0difsn  12562  hashf1lem1  13051  rlimrege0  14107  rlimrecl  14108  sumrblem  14238  fsumcvg  14239  summolem2a  14242  fsumss  14252  fsumless  14318  cvgcmpce  14340  binomlem  14349  incexclem  14356  incexc  14357  isumltss  14368  prodrblem  14447  fprodcvg  14448  prodmolem2a  14452  fprodss  14466  fprodn0f  14510  fprodeq0g  14513  fprodmodd  14516  rpnnen2lem10  14740  rpnnen2lem11  14741  sumeven  14897  sumodd  14898  lcmfunsnlem2  15140  oddprmge3  15199  oddprm  15302  nnoddn2prm  15303  nnoddn2prmb  15305  iserodd  15327  prmreclem2  15408  prmreclem3  15409  prmreclem5  15411  4sqlem19  15454  prmdvdsprmo  15533  prmodvdslcmf  15538  prmlem0  15599  firest  15865  grpinvnzcl  17259  symgextfv  17610  pmtrf  17647  pmtrdifellem3  17670  sylow2alem2  17805  sylow2a  17806  efgsf  17914  efgsrel  17919  efgs1  17920  efgsfo  17924  efgredlemc  17930  gsumzaddlem  18093  gsumzadd  18094  gsumzmhm  18109  gsum2d2lem  18144  dprdfadd  18191  dprdres  18199  subgdmdprd  18205  dmdprdsplitlem  18208  dmdprdsplit2lem  18216  dpjidcl  18229  ablfac1b  18241  pgpfac1lem1  18245  gsummgp0  18380  isirred  18471  irredrmul  18479  isdrng2  18529  isdrngd  18544  lcomfsupp  18675  lbspropd  18869  lspsneq  18892  lsppratlem6  18922  lbsextlem2  18929  lbsextlem4  18931  ringelnzr  19036  psrbaglesupp  19138  psrlidm  19173  psrridm  19174  mplsubglem  19204  mpllsslem  19205  mplsubrglem  19209  mplmonmul  19234  mplcoe1  19235  mplcoe5  19238  mplbas2  19240  evlslem3  19284  coe1tmmul2  19416  coe1tmmul  19417  xrs1mnd  19552  xrs10  19553  xrs1cmn  19554  cnsubrg  19574  psgnodpm  19701  zrhpsgnodpm  19705  evpmodpmf1o  19709  uvcresum  19899  frlmssuvc1  19900  frlmsslsp  19902  frlmup2  19905  lindfrn  19927  f1lindf  19928  lindfmm  19933  islindf4  19944  dmatmul  20070  1marepvsma1  20156  mdetdiaglem  20171  mdetrlin  20175  mdetrsca  20176  mdetralt  20181  maducoeval2  20213  madugsum  20216  symgmatr01  20227  gsummatr01lem3  20230  gsummatr01lem4  20231  gsummatr01  20232  smadiadetlem0  20234  smadiadetlem1a  20236  cmpfi  20969  2ndcdisj2  21018  elptr2  21135  ptcnplem  21182  xkopt  21216  kqdisj  21293  fin1aufil  21494  ptcmplem2  21615  ptcmplem3  21616  ptcmplem4  21617  opnsubg  21669  lpbl  22066  blcld  22068  zcld  22372  recld2  22373  reconnlem1  22385  divcn  22427  iundisj  23068  mbfeqalem  23160  itg1val2  23202  itg1ge0  23204  i1fmullem  23212  i1fadd  23213  itg1addlem4  23217  itg1mulc  23222  itg1lea  23230  itg1le  23231  mbfi1fseqlem4  23236  itg2uba  23261  itg2lea  23262  itg2eqa  23263  itg2splitlem  23266  itg2split  23267  itgeqa  23331  ellimc3  23394  dvaddbr  23452  dvmulbr  23453  dvcobr  23460  dvcjbr  23463  dvrec  23469  dvcnvlem  23488  dvexp3  23490  dveflem  23491  tdeglem4  23569  deg1n0ima  23598  deg1mul3le  23625  ig1peu  23680  ply1termlem  23708  plypf1  23717  plyaddlem1  23718  plymullem1  23719  coeeulem  23729  coeidlem  23742  coeid3  23745  coefv0  23753  coemulhi  23759  coemulc  23760  dvply1  23788  fta1  23812  vieta1lem2  23815  elaa  23820  elqaalem2  23824  aannenlem2  23833  aaliou2  23844  tayl0  23865  dvtaylp  23873  taylthlem1  23876  taylthlem2  23877  pserdvlem2  23931  logbcl  24250  relogbreexp  24258  relogbcxp  24268  cxplogb  24269  dcubic  24318  rlimcnp  24437  jensen  24460  dmgmaddn0  24494  dmlogdmgm  24495  lgamgulmlem2  24501  igamz  24519  gamp1  24529  regamcl  24532  wilthlem2  24540  basellem3  24554  chpub  24690  logexprlim  24695  lgslem1  24767  lgslem4  24770  lgsvalmod  24786  lgsqr  24821  lgsqrmod  24822  lgsqrmodndvds  24823  gausslemma2dlem0b  24827  gausslemma2dlem0c  24828  gausslemma2dlem0i  24834  gausslemma2dlem1a  24835  gausslemma2dlem4  24839  gausslemma2dlem5a  24840  gausslemma2dlem7  24843  gausslemma2d  24844  lgsquadlem1  24850  lgsquad2  24856  m1lgs  24858  2lgsoddprm  24886  dchrisum0fno1  24945  rplogsum  24961  ishpg  25397  cusgraexi  25791  uvtxnbgra  25815  cusconngra  25998  frgrancvvdeqlem9  26362  frgrancvvdeq  26363  frgrancvvdgeq  26364  2spotiundisj  26383  frghash2spot  26384  strlem1  28327  strlem3  28330  strlem4  28331  strlem5  28332  hstrlem3  28338  hstrlem4  28339  iundisjf  28618  suppss3  28724  iundisjfi  28776  qtophaus  29065  elzdif0  29186  ind0  29243  measvunilem  29436  sibfof  29563  eulerpartlemb  29591  eulerpartlemf  29593  sseqf  29615  ballotlem5  29722  ballotlemi1  29725  ballotlemii  29726  ballotlemic  29729  ballotlem1c  29730  ballotlemscr  29741  ballotlemro  29745  ballotlemfg  29748  ballotlemfrc  29749  ballotlemfrceq  29751  ballotlemrinv0  29755  plymulx0  29784  signstfvn  29806  bnj923  29926  bnj570  30063  bnj594  30070  subfacp1lem1  30249  mrsubcn  30504  mrsubco  30506  circum  30656  dfon2lem6  30771  neibastop1  31358  bj-restn0b  32049  lindsenlbs  32398  matunitlindflem1  32399  poimirlem24  32427  poimirlem25  32428  dvtan  32454  itg2addnclem2  32456  ftc1cnnc  32478  dvasin  32490  dvreasin  32492  dvreacos  32493  isdrngo2  32751  isdrngo3  32752  divrngidl  32821  isfldidl  32861  pridlc2  32865  pridlc3  32866  prter2  33008  lsateln0  33124  lsatlss  33125  lsmsat  33137  lsatcv0  33160  lsat0cv  33162  lcv1  33170  l1cvpat  33183  dih1dimatlem  35460  dihatexv2  35470  djhcvat42  35546  dihjat1lem  35559  dochsatshp  35582  lcfl6  35631  mapdrvallem2  35776  mapdpglem32  35836  irrapx1  36234  pell1234qrne0  36259  pell1234qrreccl  36260  pell1234qrmulcl  36261  pell14qrgt0  36265  pell1234qrdich  36267  pell14qrdich  36275  pell1qrge1  36276  pell1qr1  36277  pell1qrgap  36280  pell14qrgapw  36282  pellqrexplicit  36283  pellqrex  36285  pellfundge  36288  pellfundgt1  36289  setindtr  36433  kelac1  36475  mpaaeu  36563  flcidc  36587  cntzsdrg  36615  deg1mhm  36628  radcnvrat  37359  binomcxplemdvbinom  37398  disjiun2  38075  fiiuncl  38083  disjf1o  38197  difmapsn  38223  icoiccdif  38421  iccdificc  38437  fsumnncl  38462  fsumsplit1  38463  fsumsupp0  38469  fprod0  38487  climrec  38494  islpcn  38530  lptre2pt  38531  limclner  38542  fprodcncf  38611  dvrecg  38624  fperdvper  38632  dvdivcncf  38641  dvnmul  38657  dvmptfprodlem  38658  dvnprodlem2  38661  stoweidlem25  38742  stoweidlem28  38745  stoweidlem41  38758  stoweidlem44  38761  stoweidlem46  38763  stirlinglem5  38795  dirkercncflem1  38820  dirkercncflem2  38821  fourierdlem24  38848  fourierdlem62  38885  fouriersw  38948  fouriercn  38949  elaa2lem  38950  elaa2  38951  etransclem25  38976  etransclem35  38986  etransclem44  38995  sge0iunmptlemfi  39130  sge0fodjrnlem  39133  iundjiunlem  39176  meadjiunlem  39182  meaiininclem  39200  isomenndlem  39244  hsphoidmvle2  39299  hsphoidmvle  39300  hoidmv1lelem2  39306  hoidmvle  39314  ovnhoilem1  39315  hspdifhsp  39330  hspmbllem2  39341  ovnsubadd2lem  39359  ovolval4lem1  39363  preimagelt  39413  preimalegt  39414  odz2prm2pw  39838  fmtnoprmfac1lem  39839  fmtnoprmfac2lem1  39841  2pwp1prm  39866  lighneallem2  39886  lighneallem3  39887  lighneallem4  39890  bgoldbtbndlem2  40047  bgoldbtbndlem3  40048  bgoldbtbndlem4  40049  bgoldbtbnd  40050  fsummsndifre  40241  fsummmodsndifre  40243  umgrislfupgrlem  40369  usgruspgrb  40433  nbumgrvtx  40590  nbupgrres  40614  isuvtxa  40643  cusgrexi  40684  cusgrres  40686  cusgrfilem2  40694  cusconngr  41380  2pthfrgr  41476  frgrncvvdeq  41502  frgrhash2wsp  41519  c0rhm  41724  c0rnghm  41725  zrrnghm  41729  2zrngnmlid2  41763  zrinitorngc  41814  zrtermorngc  41815  mgpsumunsn  41955  mgpsumz  41956  mgpsumn  41957  lindslinindsimp1  42062  lindslinindsimp2  42068  lincresunit1  42082  lincresunit2  42083  lincresunit3lem1  42084  lincresunit3lem2  42085  lincresunit3  42086  lindssnlvec  42091  logcxp0  42149  relogbmulbexp  42175  relogbdivb  42176  dignn0fr  42215
  Copyright terms: Public domain W3C validator