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

Theorem ne0d 4305
Description: Deduction form of ne0i 4304. 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 4304 . 2 (𝐵𝐴𝐴 ≠ ∅)
31, 2syl 17 1 (𝜑𝐴 ≠ ∅)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wne 3021  c0 4295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-ne 3022  df-dif 3943  df-nul 4296
This theorem is referenced by:  snnzg  4709  prnzg  4712  exss  5352  isofrlem  7085  fvmpocurryd  7928  onnseq  7972  oeoalem  8212  oeoelem  8214  oeeui  8218  nnawordex  8253  omxpenlem  8607  frfi  8752  supgtoreq  8923  infltoreq  8955  cantnfp1lem2  9131  cantnfp1lem3  9132  oemapvali  9136  cantnflem1a  9137  cantnflem1d  9140  cantnflem1  9141  epfrs  9162  dfac9  9551  axdc3lem4  9864  intwun  10146  r1limwun  10147  gruina  10229  grur1a  10230  mulclpi  10304  indpi  10318  supsrlem  10522  axpre-sup  10580  supfirege  11616  uzn0  12249  suprzub  12328  fzn0  12911  flval3  13175  icopnfsup  13223  hashelne0d  13719  dfrtrcl2  14411  sqrlem3  14594  isercolllem2  15012  isercolllem3  15013  climsup  15016  mertenslem2  15231  gcdcllem1  15838  pclem  16165  prmreclem1  16242  4sqlem13  16283  vdwmc2  16305  vdwlem6  16312  vdwnnlem3  16323  prmgaplem3  16379  prmgaplem4  16380  mrcflem  16867  mrcval  16871  iscatd2  16942  mndbn0  17915  grpbn0  18062  issubgrpd2  18225  issubg4  18228  subgint  18233  nmzsubg  18247  cycsubgcl  18279  ghmpreima  18310  gastacl  18369  sylow1lem5  18647  pgpssslw  18659  sylow2alem2  18663  sylow2blem3  18667  fislw  18670  sylow3lem4  18675  torsubg  18894  oddvdssubg  18895  iscygd  18926  iscygodd  18927  dprdsubg  19066  ablfac1eu  19115  simpgnideld  19141  cntzsubr  19488  primefld  19504  primefld0cl  19505  primefld1cl  19506  islss4  19654  lss1d  19655  lssintcl  19656  lspsolvlem  19834  lbsextlem1  19850  lidlsubg  19907  abvn0b  19994  psrbas  20077  mplsubglem  20133  mplind  20200  mhpsubg  20257  zringlpirlem1  20547  ocvlss  20732  lmiclbs  20897  lmisfree  20902  mat1ric  21012  dmatsgrp  21024  scmatsgrp  21044  scmatsgrp1  21047  scmatlss  21050  scmatric  21062  cpmatsubgpmat  21244  matcpmric  21283  pmmpric  21347  clscld  21571  2ndcdisj  21980  dfac14lem  22141  opnfbas  22366  isfil2  22380  filn0  22386  filssufilg  22435  rnelfmlem  22476  flimfnfcls  22552  ptcmplem2  22577  clssubg  22632  tgpconncomp  22636  tsmsfbas  22651  ustfilxp  22736  ustne0  22737  xbln0  22939  bln0  22940  metustfbas  23082  metustbl  23091  nrgdomn  23195  icccmplem2  23346  icccmplem3  23347  reconnlem2  23350  phtpcer  23514  reparpht  23517  phtpcco2  23518  pcohtpy  23539  pcorevlem  23545  isclmp  23616  iscmet3lem2  23810  bcthlem4  23845  minveclem3b  23946  ivthlem2  23968  ivthlem3  23969  evthicc  23975  ovollb2  24005  ovolunlem1a  24012  ovolunlem1  24013  ovoliunlem1  24018  ovoliun2  24022  ioombl1lem4  24077  uniioombllem1  24097  uniioombllem2  24099  uniioombllem6  24104  mbfsup  24180  mbfinf  24181  mbflimsup  24182  itg2monolem1  24266  itg2mono  24269  ulm0  24894  pilem2  24955  pilem3  24956  ftalem3  25566  ftalem4  25567  ftalem5  25568  dchrabs  25750  pntlem3  26099  tglnne0  26340  axlowdim1  26659  nvo00  28452  nmorepnf  28459  minvecolem1  28565  submomnd  30625  cycpmco2lem5  30686  primefldchr  30781  suborng  30802  ordtconnlem1  31053  rrhre  31148  sigagenval  31285  oddpwdc  31498  bnj1177  32162  bnj1523  32227  erdszelem8  32329  txsconnlem  32371  cvxsconn  32374  cvmsss2  32405  cvmliftmolem2  32413  cvmlift2lem12  32445  cvmliftpht  32449  nocvxminlem  33131  finminlem  33550  onint1  33681  finxpreclem4  34544  heicant  34794  itg2addnc  34813  ftc1anclem7  34840  ftc1anc  34842  prdsbnd2  34941  lkrlss  36098  pclvalN  36893  dian0  38042  docaclN  38127  dicn0  38195  dihglblem5  38301  dihglb2  38345  doch2val2  38367  dochocss  38369  lclkr  38536  lclkrs  38542  lcfr  38588  qsalrel  38990  nacsfix  39174  mzpcln0  39190  rencldnfilem  39282  fnwe2lem2  39516  kelac1  39528  harn0  39567  hbtlem2  39589  gneispa  40345  scottrankd  40449  ubelsupr  41142  suprnmpt  41295  disjinfi  41319  suprubrnmpt2  41389  suprubrnmpt  41390  ssfiunibd  41441  allbutfi  41530  allbutfiinf  41559  uzn0d  41564  uzublem  41569  climinf  41752  limclr  41801  climinf2lem  41852  limsupubuzlem  41858  liminflelimsupuz  41931  cnrefiisplem  41975  ioodvbdlimc1lem1  42081  ioodvbdlimc1  42083  ioodvbdlimc2  42085  stoweidlem36  42187  fourierdlem20  42278  fourierdlem25  42283  fourierdlem31  42289  fourierdlem37  42295  fourierdlem46  42303  fourierdlem52  42309  fourierdlem54  42311  fouriercn  42383  elaa2lem  42384  salgenval  42472  salgenn0  42480  sge0isum  42575  sge0reuzb  42596  ovnlerp  42710  ovnf  42711  hsphoidmvle2  42733  hsphoidmvle  42734  hoiprodp1  42736  hoidmv1lelem1  42739  hoidmv1lelem3  42741  hoidmv1le  42742  hoidifhspdmvle  42768  hspmbllem1  42774  hspmbllem3  42776  ovnovollem2  42805  smflimlem1  42913  smfsuplem1  42951  smfsuplem3  42953  smflimsuplem5  42964  smflimsuplem7  42966  lincolss  44321
  Copyright terms: Public domain W3C validator