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

Theorem eldifi 4086
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 3920 . 2 (𝐴 ∈ (𝐵𝐶) ↔ (𝐴𝐵 ∧ ¬ 𝐴𝐶))
21simplbi 498 1 (𝐴 ∈ (𝐵𝐶) → 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2106  cdif 3907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3447  df-dif 3913
This theorem is referenced by:  difss  4091  eqoreldif  4645  xpdifid  6120  tz7.7  6343  tfi  7789  peano5  7830  peano5OLD  7831  xpord2pred  8077  frrlem12  8228  frrlem13  8229  wfrlem10OLD  8264  wfrlem15OLD  8269  tz7.48-1  8389  tz7.49  8391  dif20el  8451  oaf1o  8510  oeordi  8534  oeord  8535  oecan  8536  oeword  8537  oeworde  8540  oelimcl  8547  oeeulem  8548  oeeui  8549  oaabs2  8595  boxcutc  8879  domdifsn  8998  pssnn  9112  pwfilem  9121  isinf  9204  isinfOLD  9205  pssnnOLD  9209  pwfilemOLD  9290  fsuppco2  9339  fsuppcor  9340  ordtypelem7  9460  unxpwdom2  9524  inf3lem3  9566  cantnfp1lem1  9614  cantnfp1lem3  9616  ttrcltr  9652  infxpenc2lem1  9955  dfacacn  10077  isf32lem3  10291  isf34lem4  10313  fin67  10331  isfin7-2  10332  domtriomlem  10378  axdc2lem  10384  axdc3lem4  10389  axdc4lem  10391  ttukeylem7  10451  konigthlem  10504  fpwwe2lem12  10578  fpwwe2  10579  modfzo0difsn  13848  hashf1lem1  14353  hashf1lem1OLD  14354  hashle2prv  14377  rlimrege0  15461  rlimrecl  15462  sumrblem  15596  fsumcvg  15597  summolem2a  15600  fsumss  15610  fsumsplit1  15630  fsumless  15681  cvgcmpce  15703  binomlem  15714  incexclem  15721  incexc  15722  isumltss  15733  prodrblem  15812  fprodcvg  15813  prodmolem2a  15817  fprodss  15831  fprodn0f  15874  fprodeq0g  15877  fprodmodd  15880  rpnnen2lem10  16105  rpnnen2lem11  16106  sumeven  16269  sumodd  16270  lcmfunsnlem2  16516  oddprmge3  16576  oddprm  16682  nnoddn2prm  16683  nnoddn2prmb  16685  iserodd  16707  prmreclem2  16789  prmreclem3  16790  prmreclem5  16792  4sqlem19  16835  prmdvdsprmo  16914  prmodvdslcmf  16919  prmlem0  16978  firest  17314  grpinvnzcl  18819  symgextfv  19200  pmtrf  19237  pmtrdifellem3  19260  sylow2alem2  19400  sylow2a  19401  efgsf  19511  efgsrel  19516  efgs1  19517  efgsfo  19521  gsumzaddlem  19698  gsumzadd  19699  gsumzmhm  19714  gsum2d2lem  19750  dprdfadd  19799  dprdres  19807  subgdmdprd  19813  dmdprdsplitlem  19816  dmdprdsplit2lem  19824  dpjidcl  19837  ablfac1b  19849  pgpfac1lem1  19853  gsummgp0  20032  isirred  20128  irredrmul  20136  isdrng2  20198  isdrngd  20214  cntzsdrg  20269  lcomfsupp  20362  lbspropd  20560  lspsneq  20583  lsppratlem6  20613  lbsextlem2  20620  lbsextlem4  20622  ringelnzr  20736  xrs1mnd  20835  xrs10  20836  xrs1cmn  20837  cnsubrg  20857  psgnodpm  20992  zrhpsgnodpm  20996  evpmodpmf1o  21000  uvcresum  21199  frlmssuvc1  21200  frlmsslsp  21202  frlmup2  21205  lindfrn  21227  f1lindf  21228  lindfmm  21233  islindf4  21244  psrbaglesupp  21326  psrbaglesuppOLD  21327  psrlidm  21372  psrridm  21373  mplsubglem  21405  mpllsslem  21406  mplsubrglem  21410  mplmonmul  21437  mplcoe1  21438  mplcoe5  21441  mplbas2  21443  evlslem3  21490  mhpvscacl  21544  coe1tmmul2  21647  coe1tmmul  21648  dmatmul  21846  1marepvsma1  21932  mdetdiaglem  21947  mdetrlin  21951  mdetrsca  21952  mdetralt  21957  maducoeval2  21989  madugsum  21992  symgmatr01  22003  gsummatr01lem3  22006  gsummatr01lem4  22007  gsummatr01  22008  smadiadetlem0  22010  smadiadetlem1a  22012  cmpfi  22759  2ndcdisj2  22808  elptr2  22925  ptcnplem  22972  xkopt  23006  kqdisj  23083  fin1aufil  23283  ptcmplem2  23404  ptcmplem3  23405  ptcmplem4  23406  opnsubg  23459  lpbl  23859  blcld  23861  zcld  24176  recld2  24177  reconnlem1  24189  divcn  24231  iundisj  24912  mbfeqalem1  25005  itg1val2  25048  itg1ge0  25050  i1fmullem  25058  i1fadd  25059  itg1addlem4  25063  itg1addlem4OLD  25064  itg1mulc  25069  itg1lea  25077  itg1le  25078  mbfi1fseqlem4  25083  itg2uba  25108  itg2lea  25109  itg2eqa  25110  itg2splitlem  25113  itg2split  25114  itgeqa  25178  ellimc3  25243  dvaddbr  25302  dvmulbr  25303  dvcobr  25310  dvcjbr  25313  dvrec  25319  dvrecg  25337  dvcnvlem  25340  dvexp3  25342  dveflem  25343  tdeglem4  25424  tdeglem4OLD  25425  deg1n0ima  25454  deg1mul3le  25481  ig1peu  25536  ply1termlem  25564  plypf1  25573  plyaddlem1  25574  plymullem1  25575  coeeulem  25585  coeidlem  25598  coeid3  25601  coefv0  25609  coemulhi  25615  coemulc  25616  dvply1  25644  fta1  25668  vieta1lem2  25671  elaa  25676  elqaalem2  25680  aannenlem2  25689  aaliou2  25700  tayl0  25721  dvtaylp  25729  taylthlem1  25732  taylthlem2  25733  pserdvlem2  25787  logbcl  26117  relogbreexp  26125  relogbcxp  26135  cxplogb  26136  dcubic  26196  rlimcnp  26315  jensen  26338  dmgmaddn0  26372  dmlogdmgm  26373  lgamgulmlem2  26379  igamz  26397  gamp1  26407  regamcl  26410  wilthlem2  26418  basellem3  26432  chpub  26568  logexprlim  26573  lgslem1  26645  lgslem4  26648  lgsvalmod  26664  lgsqr  26699  lgsqrmod  26700  lgsqrmodndvds  26701  gausslemma2dlem0b  26705  gausslemma2dlem0c  26706  gausslemma2dlem0i  26712  gausslemma2dlem1a  26713  gausslemma2dlem4  26717  gausslemma2dlem5a  26718  gausslemma2dlem7  26721  gausslemma2d  26722  lgsquad2  26734  m1lgs  26736  2lgsoddprm  26764  2sqreultblem  26796  dchrisum0fno1  26859  rplogsum  26875  ishpg  27701  elntg2  27934  umgrislfupgrlem  28073  usgruspgrb  28132  nbumgrvtx  28294  nbupgrres  28312  isuvtx  28343  cusgrexilem2  28390  cusgrexi  28391  structtocusgr  28394  cusgrres  28396  cusgrfilem2  28404  vtxdginducedm1  28491  cusconngr  29135  2pthfrgr  29228  frgrncvvdeq  29253  frgrwopreglem4  29259  frgrwopreglem5  29265  frgrwopreg  29267  frgrhash2wsp  29276  strlem1  31192  strlem3  31195  strlem4  31196  strlem5  31197  hstrlem3  31203  hstrlem4  31204  iundisjf  31507  suppss3  31641  iundisjfi  31699  irngnzply1  32365  qtophaus  32417  elzdif0  32561  ind0  32617  measvunilem  32811  sibfof  32940  eulerpartlemb  32968  eulerpartlemf  32970  sseqf  32992  ballotlem5  33099  ballotlemi1  33102  ballotlemii  33103  ballotlemic  33106  ballotlem1c  33107  ballotlemscr  33118  ballotlemro  33122  ballotlemfg  33125  ballotlemfrc  33126  ballotlemfrceq  33128  ballotlemrinv0  33132  plymulx0  33159  signstfvn  33181  signsvfn  33194  bnj923  33380  bnj570  33517  bnj594  33524  subfacp1lem1  33773  satffunlem2lem1  33998  mrsubcn  34113  mrsubco  34115  circum  34262  dfon2lem6  34363  neibastop1  34831  bj-restn0b  35562  lindsadd  36071  lindsenlbs  36073  matunitlindflem1  36074  poimirlem24  36102  poimirlem25  36103  dvtan  36128  itg2addnclem2  36130  ftc1cnnc  36150  dvasin  36162  dvreasin  36164  dvreacos  36165  isdrngo2  36417  isdrngo3  36418  divrngidl  36487  isfldidl  36527  pridlc2  36531  pridlc3  36532  prter2  37343  lsateln0  37457  lsatlss  37458  lsmsat  37470  lsatcv0  37493  lsat0cv  37495  lcv1  37503  l1cvpat  37516  dih1dimatlem  39792  dihatexv2  39802  djhcvat42  39878  dihjat1lem  39891  dochsatshp  39914  lcfl6  39963  mapdrvallem2  40108  mapdpglem32  40168  sticksstones22  40576  isdomn4  40624  evlsbagval  40736  prjspertr  40929  prjsperref  40930  prjspersym  40931  prjspvs  40934  prjsprellsp  40935  dffltz  40958  irrapx1  41137  pell1234qrne0  41162  pell1234qrreccl  41163  pell1234qrmulcl  41164  pell14qrgt0  41168  pell1234qrdich  41170  pell14qrdich  41178  pell1qrge1  41179  pell1qr1  41180  pell1qrgap  41183  pell14qrgapw  41185  pellqrexplicit  41186  pellqrex  41188  pellfundge  41191  pellfundgt1  41192  setindtr  41334  kelac1  41376  mpaaeu  41463  flcidc  41487  deg1mhm  41520  onexoegt  41564  cantnfub  41641  cantnfresb  41644  succlg  41648  dflim5  41649  omabs2  41651  minregex2  41797  radcnvrat  42584  binomcxplemdvbinom  42623  disjiun2  43256  fiiuncl  43263  disjf1o  43400  difmapsn  43423  supminfxr2  43694  icoiccdif  43752  iccdificc  43767  fsumnncl  43803  fsumsupp0  43809  fprod0  43827  climrec  43834  islpcn  43870  lptre2pt  43871  limclner  43882  cnrefiisplem  44060  fprodcncf  44131  fperdvper  44150  dvdivcncf  44158  dvnmul  44174  dvmptfprodlem  44175  dvnprodlem2  44178  stoweidlem25  44256  stoweidlem28  44259  stoweidlem41  44272  stoweidlem44  44275  stoweidlem46  44277  stirlinglem5  44309  dirkercncflem1  44334  dirkercncflem2  44335  fourierdlem24  44362  fourierdlem62  44399  fouriersw  44462  fouriercn  44463  elaa2lem  44464  elaa2  44465  etransclem25  44490  etransclem35  44500  etransclem44  44509  sge0iunmptlemfi  44644  sge0fodjrnlem  44647  iundjiunlem  44690  meadjiunlem  44696  meaiininclem  44717  isomenndlem  44761  hsphoidmvle2  44816  hsphoidmvle  44817  hoidmv1lelem2  44823  hoidmvle  44831  ovnhoilem1  44832  hspdifhsp  44847  hspmbllem2  44858  ovnsubadd2lem  44876  ovolval4lem1  44880  preimagelt  44930  preimalegt  44931  fsummsndifre  45554  fsummmodsndifre  45556  odz2prm2pw  45745  fmtnoprmfac1lem  45746  fmtnoprmfac2lem1  45748  2pwp1prm  45771  lighneallem2  45788  lighneallem3  45789  lighneallem4  45792  bgoldbtbndlem2  45988  bgoldbtbndlem3  45989  bgoldbtbndlem4  45990  bgoldbtbnd  45991  c0rhm  46200  c0rnghm  46201  zrrnghm  46205  2zrngnmlid2  46239  zrinitorngc  46288  zrtermorngc  46289  mgpsumunsn  46427  mgpsumz  46428  mgpsumn  46429  lindslinindsimp1  46528  lindslinindsimp2  46534  lincresunit1  46548  lincresunit2  46549  lincresunit3lem1  46550  lincresunit3lem2  46551  lincresunit3  46552  lindssnlvec  46557  logcxp0  46611  relogbmulbexp  46637  relogbdivb  46638  dignn0fr  46677  rrxlinesc  46811  eenglngeehlnmlem1  46813  eenglngeehlnmlem2  46814
  Copyright terms: Public domain W3C validator