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

Theorem ne0d 4296
Description: Deduction form of ne0i 4295. If a class has elements, then it is nonempty. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
Hypothesis
Ref Expression
ne0d.1 (𝜑𝐵𝐴)
Assertion
Ref Expression
ne0d (𝜑𝐴 ≠ ∅)

Proof of Theorem ne0d
StepHypRef Expression
1 ne0d.1 . 2 (𝜑𝐵𝐴)
2 ne0i 4295 . 2 (𝐵𝐴𝐴 ≠ ∅)
31, 2syl 17 1 (𝜑𝐴 ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wne 2944  c0 4283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-dif 3914  df-nul 4284
This theorem is referenced by:  snnzg  4736  prnzg  4740  exss  5421  isofrlem  7286  fvmpocurryd  8203  onnseq  8291  oeoalem  8544  oeoelem  8546  oeeui  8550  nnawordex  8585  omxpenlem  9018  frfi  9233  supgtoreq  9407  infltoreq  9439  cantnfp1lem2  9616  cantnfp1lem3  9617  oemapvali  9621  cantnflem1a  9622  cantnflem1d  9625  cantnflem1  9626  epfrs  9668  dfac9  10073  axdc3lem4  10390  intwun  10672  r1limwun  10673  gruina  10755  grur1a  10756  mulclpi  10830  indpi  10844  supsrlem  11048  axpre-sup  11106  supfirege  12143  uzn0  12781  suprzub  12865  fzn0  13456  flval3  13721  icopnfsup  13771  hashelne0d  14269  dfrtrcl2  14948  01sqrexlem3  15130  isercolllem2  15551  isercolllem3  15552  climsup  15555  mertenslem2  15771  gcdcllem1  16380  pclem  16711  prmreclem1  16789  4sqlem13  16830  vdwmc2  16852  vdwlem6  16859  vdwnnlem3  16870  prmgaplem3  16926  prmgaplem4  16927  mrcflem  17487  mrcval  17491  iscatd2  17562  mndbn0  18573  grpbn0  18780  issubgrpd2  18945  issubg4  18948  subgint  18953  nmzsubg  18968  cycsubgcl  19000  ghmpreima  19031  gastacl  19090  sylow1lem5  19385  pgpssslw  19397  sylow2alem2  19401  sylow2blem3  19405  fislw  19408  sylow3lem4  19413  torsubg  19633  oddvdssubg  19634  iscygd  19665  iscygodd  19666  dprdsubg  19804  ablfac1eu  19853  simpgnideld  19879  cntzsubr  20258  primefld  20275  primefld0cl  20276  primefld1cl  20277  islss4  20426  lss1d  20427  lssintcl  20428  lspsolvlem  20606  lbsextlem1  20622  lidlsubg  20688  abvn0b  20775  zringlpirlem1  20886  ocvlss  21079  lmiclbs  21246  lmisfree  21251  psrbas  21349  mplsubglem  21408  mplind  21481  mhpsubg  21546  mat1ric  21839  dmatsgrp  21851  scmatsgrp  21871  scmatsgrp1  21874  scmatlss  21877  scmatric  21889  cpmatsubgpmat  22072  matcpmric  22111  pmmpric  22175  clscld  22401  2ndcdisj  22810  dfac14lem  22971  opnfbas  23196  isfil2  23210  filn0  23216  filssufilg  23265  rnelfmlem  23306  flimfnfcls  23382  ptcmplem2  23407  clssubg  23463  tgpconncomp  23467  tsmsfbas  23482  ustfilxp  23567  ustne0  23568  xbln0  23770  bln0  23771  metustfbas  23916  metustbl  23925  nrgdomn  24038  icccmplem2  24189  icccmplem3  24190  reconnlem2  24193  phtpcer  24361  reparpht  24364  phtpcco2  24365  pcohtpy  24386  pcorevlem  24392  isclmp  24463  iscmet3lem2  24659  bcthlem4  24694  minveclem3b  24795  ivthlem2  24819  ivthlem3  24820  evthicc  24826  ovollb2  24856  ovolunlem1a  24863  ovolunlem1  24864  ovoliunlem1  24869  ovoliun2  24873  ioombl1lem4  24928  uniioombllem1  24948  uniioombllem2  24950  uniioombllem6  24955  mbfsup  25031  mbfinf  25032  mbflimsup  25033  itg2monolem1  25118  itg2mono  25121  ulm0  25753  pilem2  25814  pilem3  25815  ftalem3  26427  ftalem4  26428  ftalem5  26429  dchrabs  26611  pntlem3  26960  nocvxminlem  27120  tglnne0  27585  axlowdim1  27911  nvo00  29706  nmorepnf  29713  minvecolem1  29819  submomnd  31921  cycpmco2lem5  31982  primefldchr  32081  fldgensdrg  32086  suborng  32113  nsgqusf1olem1  32194  intlidl  32202  rhmpreimaidl  32203  idlinsubrg  32208  rhmimaidl  32209  ssmxidl  32242  ordtconnlem1  32508  rrhre  32605  sigagenval  32742  oddpwdc  32957  bnj1177  33621  bnj1523  33686  erdszelem8  33795  txsconnlem  33837  cvxsconn  33840  cvmsss2  33871  cvmliftmolem2  33879  cvmlift2lem12  33911  cvmliftpht  33915  finminlem  34793  onint1  34924  finxpreclem4  35868  heicant  36116  itg2addnc  36135  ftc1anclem7  36160  ftc1anc  36162  prdsbnd2  36257  lkrlss  37560  pclvalN  38356  dian0  39505  docaclN  39590  dicn0  39658  dihglblem5  39764  dihglb2  39808  doch2val2  39830  dochocss  39832  lclkr  39999  lclkrs  40005  lcfr  40051  qsalrel  40667  imadrhmcl  40719  nacsfix  41038  mzpcln0  41054  rencldnfilem  41146  fnwe2lem2  41381  kelac1  41393  harn0  41432  hbtlem2  41454  gneispa  42409  scottrankd  42535  ubelsupr  43232  suprnmpt  43398  disjinfi  43419  suprubrnmpt2  43487  suprubrnmpt  43488  ssfiunibd  43550  allbutfi  43635  allbutfiinf  43662  uzn0d  43667  uzublem  43672  climinf  43854  limclr  43903  climinf2lem  43954  limsupubuzlem  43960  liminflelimsupuz  44033  cnrefiisplem  44077  ioodvbdlimc1lem1  44179  ioodvbdlimc1  44181  ioodvbdlimc2  44183  stoweidlem36  44284  fourierdlem20  44375  fourierdlem25  44380  fourierdlem31  44386  fourierdlem37  44392  fourierdlem46  44400  fourierdlem52  44406  fourierdlem54  44408  fouriercn  44480  elaa2lem  44481  salgenval  44569  salgenn0  44579  sge0isum  44675  sge0reuzb  44696  ovnlerp  44810  ovnf  44811  hsphoidmvle2  44833  hsphoidmvle  44834  hoiprodp1  44836  hoidmv1lelem1  44839  hoidmv1lelem3  44841  hoidmv1le  44842  hoidifhspdmvle  44868  hspmbllem1  44874  hspmbllem3  44876  ovnovollem2  44905  smflimlem1  45019  smfsuplem1  45059  smfsuplem3  45061  smflimsuplem5  45072  smflimsuplem7  45074  preimafvn0  45579  lincolss  46522  fvconstr2  46931  catprs  47038
  Copyright terms: Public domain W3C validator