Theorem ne0d 4291

Description: Deduction form of ne0i 4290. 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

Step	Hyp	Ref	Expression
1		ne0d.1	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
2		ne0i 4290	. 2 ⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝐴 ≠ ∅)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ≠ wne 2959  ∅c0 4281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-dif 4050  df-nul 4282

This theorem is used by:  snnzg  4735  prnzg  4739  eqsnd  4789  exss  5436  isofrlem  7374  peano3  7929  fnwe2lem3  8177  fvmpocurryd  8319  onnseq  8383  oeoalem  8636  oeoelem  8638  oeeui  8642  nnawordex  8677  omxpenlem  9128  frfi  9307  supgtoreq  9493  infltoreq  9526  cantnfp1lem2  9710  cantnfp1lem3  9711  oemapvali  9715  cantnflem1a  9716  cantnflem1d  9719  cantnflem1  9720  epfrs  9762  rankfilimbi  9932  scottrankd  9979  dfac9  10245  axdc3lem4  10561  intwun  10850  r1limwun  10851  gruina  10933  grur1a  10934  mulclpi  11008  indpi  11022  supsrlem  11226  axpre-sup  11284  supfirege  12334  uzn0  13012  suprzub  13096  fzn0  13701  flval3  13985  icopnfsup  14035  hashelne0d  14542  dfrtrcl2  15247  01sqrexlem3  15443  isercolllem2  15865  isercolllem3  15866  climsup  15869  mertenslem2  16086  gcdcllem1  16701  pclem  17048  prmreclem1  17126  4sqlem13  17167  vdwmc2  17189  vdwlem6  17196  vdwnnlem3  17207  prmgaplem3  17263  prmgaplem4  17264  mrcflem  17812  mrcval  17816  iscatd2  17887  chnub  18828  mndbn0  18972  grpbn0  19209  issubgrpd2  19385  issubg4  19388  subgint  19393  nmzsubg  19407  cycsubgcl  19453  ghmpreima  19484  gastacl  19556  sylow1lem5  19849  pgpssslw  19861  sylow2alem2  19865  sylow2blem3  19869  fislw  19872  sylow3lem4  19877  torsubg  20101  oddvdssubg  20102  iscygd  20134  iscygodd  20135  dprdsubg  20273  ablfac1eu  20322  simpgnideld  20348  submomnd  20379  01eq0ring  20814  cntzsubrng  20852  cntzsubr  20891  imadrhmcl  21087  primefld  21095  primefld0cl  21096  primefld1cl  21097  abvn0b  21126  suborng  21166  islss4  21270  lss1d  21271  lssintcl  21272  lspsolvlem  21453  lbsextlem1  21469  dflidl2rng  21530  lidlsubg  21535  lidlunin0  21548  rhmpreimaidl  21604  ssdifidl  21674  ssdifidlprm  21675  zringlpirlem1  21801  ocvlss  22011  lmiclbs  22176  lmisfree  22181  psrbas  22275  mplsubglem  22339  mplind  22412  mhpsubg  22507  mat1ric  22835  dmatsgrp  22847  scmatsgrp  22867  scmatsgrp1  22870  scmatlss  22873  scmatric  22885  cpmatsubgpmat  23071  matcpmric  23110  pmmpric  23174  clscld  23398  2ndcdisj  23808  dfac14lem  23969  opnfbas  24194  isfil2  24208  filn0  24214  filssufilg  24263  rnelfmlem  24304  flimfnfcls  24380  ptcmplem2  24405  clssubg  24461  tgpconncomp  24465  tsmsfbas  24480  ustfilxp  24565  ustne0  24566  xbln0  24766  bln0  24767  metustfbas  24909  metustbl  24918  nrgdomn  25023  icccmplem2  25176  icccmplem3  25177  reconnlem2  25180  phtpcer  25349  reparpht  25352  phtpcco2  25353  pcohtpy  25374  pcorevlem  25380  isclmp  25451  iscmet3lem2  25646  bcthlem4  25681  minveclem3b  25782  ivthlem2  25806  ivthlem3  25807  evthicc  25813  ovollb2  25843  ovolunlem1a  25850  ovolunlem1  25851  ovoliunlem1  25856  ovoliun2  25860  ioombl1lem4  25915  uniioombllem1  25935  uniioombllem2  25937  uniioombllem6  25942  mbfsup  26018  mbfinf  26019  mbflimsup  26020  itg2monolem1  26104  itg2mono  26107  ulm0  26751  pilem2  26812  pilem3  26813  ftalem3  27435  ftalem4  27436  ftalem5  27437  dchrabs  27620  pntlem3  27969  nocvxminlem  28173  bdayfinbndlem1  28886  tglnne0  29142  tglnpt4  29156  lnoppinn0  29264  angmgmaddeu2  29413  angmgmaddeu3  29414  angmgmaddov2lem  29420  angmgmaddcpbl  29423  angmgmaddrid  29426  prlngmolem1  29463  prlngmolem2  29464  prlngmo2  29467  prlngpln4  29469  prlngsymquadlem  29474  quadcgrprlng  29477  axlowdim1  29570  nvo00  31396  nmorepnf  31403  minvecolem1  31509  wrdpmtrlast  33730  cycpmco2lem5  33767  elrgspnlem1  33879  edompidlem  33940  primefldchr  33947  fldgensdrg  33960  nsgqusf1olem1  34048  intlidl  34054  idlinsubrg  34065  rhmimaidl  34066  ssmxidl  34083  dflringlem2  34111  pidufd  34159  1arithufdlem1  34160  ply1dg1rtn0  34196  ply1degltlss  34211  exsslsb  34312  constrsdrg  34490  ordtconnlem1  34639  rrhre  34736  sigagenval  34856  oddpwdc  35069  bnj1177  35719  bnj1523  35784  erdszelem8  36143  txsconnlem  36185  cvxsconn  36188  cvmsss2  36219  cvmliftmolem2  36227  cvmlift2lem12  36259  cvmliftpht  36263  finminlem  37297  onint1  37428  weiunlem  37442  weiunfr  37446  finxpreclem4  38522  heicant  38778  itg2addnc  38797  ftc1anclem7  38822  ftc1anc  38824  prdsbnd2  38932  lkrlss  40355  pclvalN  41150  dian0  42299  docaclN  42384  dicn0  42452  dihglblem5  42558  dihglb2  42602  doch2val2  42624  dochocss  42626  lclkr  42793  lclkrs  42799  lcfr  42845  aks6d1c6lem3  43425  unitscyglem2  43449  qsalrel  43496  nacsfix  43927  mzpcln0  43943  rencldnfilem  44031  kelac1  44269  harn0  44307  hbtlem2  44329  naddwordnexlem4  44606  omltoe  44611  gneispa  45333  imo72b2lem0  45368  relpfrlem  46149  ubelsupr  46253  suprnmpt  46404  disjinfi  46422  suprubrnmpt2  46479  suprubrnmpt  46480  ssfiunibd  46540  allbutfi  46619  allbutfiinf  46645  uzn0d  46650  uzublem  46655  climinf  46833  limclr  46880  climinf2lem  46931  limsupubuzlem  46937  liminflelimsupuz  47010  cnrefiisplem  47054  ioodvbdlimc1lem1  47156  ioodvbdlimc1  47158  ioodvbdlimc2  47160  stoweidlem36  47261  fourierdlem20  47352  fourierdlem25  47357  fourierdlem31  47363  fourierdlem37  47369  fourierdlem46  47377  fourierdlem48  47379  fourierdlem49  47380  fourierdlem52  47383  fourierdlem54  47385  fouriercn  47457  elaa2lem  47458  salgenval  47546  salgenn0  47556  sge0isum  47652  sge0reuzb  47673  ovnlerp  47787  ovnf  47788  hsphoidmvle2  47810  hsphoidmvle  47811  hoiprodp1  47813  hoidmv1lelem1  47816  hoidmv1lelem3  47818  hoidmv1le  47819  hoidifhspdmvle  47845  hspmbllem1  47851  hspmbllem3  47853  ovnovollem2  47882  smflimlem1  47996  smfsuplem1  48036  smfsuplem3  48038  smflimsuplem5  48049  smflimsuplem7  48051  preimafvn0  48677  lincolss  49761  elovconstbrd  50190  catprs  50340  discsubc  50393  iinfconstbas  50395  eloppf  50464  eloppf2  50465  oppcup3  50540  oppcthinendcALT  50791  termcterm3  50865  termcciso  50866  idfudiag1bas  50874  idfudiag1  50875