Theorem ne0d 4300

Description: Deduction form of ne0i 4299. 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 4299	. 2 ⊢ (𝐵 ∈ 𝐴 → 𝐴 ≠ ∅)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ≠ ∅)

Syntax hints:   → wi 4   ∈ wcel 2110   ≠ wne 3016  ∅c0 4290

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-ne 3017  df-dif 3938  df-nul 4291

This theorem is referenced by:  snnzg  4703  prnzg  4706  exss  5347  isofrlem  7087  fvmpocurryd  7931  onnseq  7975  oeoalem  8216  oeoelem  8218  oeeui  8222  nnawordex  8257  omxpenlem  8612  frfi  8757  supgtoreq  8928  infltoreq  8960  cantnfp1lem2  9136  cantnfp1lem3  9137  oemapvali  9141  cantnflem1a  9142  cantnflem1d  9145  cantnflem1  9146  epfrs  9167  dfac9  9556  axdc3lem4  9869  intwun  10151  r1limwun  10152  gruina  10234  grur1a  10235  mulclpi  10309  indpi  10323  supsrlem  10527  axpre-sup  10585  supfirege  11621  uzn0  12254  suprzub  12333  fzn0  12915  flval3  13179  icopnfsup  13227  hashelne0d  13723  dfrtrcl2  14415  sqrlem3  14598  isercolllem2  15016  isercolllem3  15017  climsup  15020  mertenslem2  15235  gcdcllem1  15842  pclem  16169  prmreclem1  16246  4sqlem13  16287  vdwmc2  16309  vdwlem6  16316  vdwnnlem3  16327  prmgaplem3  16383  prmgaplem4  16384  mrcflem  16871  mrcval  16875  iscatd2  16946  mndbn0  17921  grpbn0  18126  issubgrpd2  18289  issubg4  18292  subgint  18297  nmzsubg  18311  cycsubgcl  18343  ghmpreima  18374  gastacl  18433  sylow1lem5  18721  pgpssslw  18733  sylow2alem2  18737  sylow2blem3  18741  fislw  18744  sylow3lem4  18749  torsubg  18968  oddvdssubg  18969  iscygd  19000  iscygodd  19001  dprdsubg  19140  ablfac1eu  19189  simpgnideld  19215  cntzsubr  19562  primefld  19578  primefld0cl  19579  primefld1cl  19580  islss4  19728  lss1d  19729  lssintcl  19730  lspsolvlem  19908  lbsextlem1  19924  lidlsubg  19982  abvn0b  20069  psrbas  20152  mplsubglem  20208  mplind  20276  mhpsubg  20334  zringlpirlem1  20625  ocvlss  20810  lmiclbs  20975  lmisfree  20980  mat1ric  21090  dmatsgrp  21102  scmatsgrp  21122  scmatsgrp1  21125  scmatlss  21128  scmatric  21140  cpmatsubgpmat  21322  matcpmric  21361  pmmpric  21425  clscld  21649  2ndcdisj  22058  dfac14lem  22219  opnfbas  22444  isfil2  22458  filn0  22464  filssufilg  22513  rnelfmlem  22554  flimfnfcls  22630  ptcmplem2  22655  clssubg  22711  tgpconncomp  22715  tsmsfbas  22730  ustfilxp  22815  ustne0  22816  xbln0  23018  bln0  23019  metustfbas  23161  metustbl  23170  nrgdomn  23274  icccmplem2  23425  icccmplem3  23426  reconnlem2  23429  phtpcer  23593  reparpht  23596  phtpcco2  23597  pcohtpy  23618  pcorevlem  23624  isclmp  23695  iscmet3lem2  23889  bcthlem4  23924  minveclem3b  24025  ivthlem2  24047  ivthlem3  24048  evthicc  24054  ovollb2  24084  ovolunlem1a  24091  ovolunlem1  24092  ovoliunlem1  24097  ovoliun2  24101  ioombl1lem4  24156  uniioombllem1  24176  uniioombllem2  24178  uniioombllem6  24183  mbfsup  24259  mbfinf  24260  mbflimsup  24261  itg2monolem1  24345  itg2mono  24348  ulm0  24973  pilem2  25034  pilem3  25035  ftalem3  25646  ftalem4  25647  ftalem5  25648  dchrabs  25830  pntlem3  26179  tglnne0  26420  axlowdim1  26739  nvo00  28532  nmorepnf  28539  minvecolem1  28645  submomnd  30706  cycpmco2lem5  30767  primefldchr  30862  suborng  30883  ssmxidl  30974  ordtconnlem1  31162  rrhre  31257  sigagenval  31394  oddpwdc  31607  bnj1177  32273  bnj1523  32338  erdszelem8  32440  txsconnlem  32482  cvxsconn  32485  cvmsss2  32516  cvmliftmolem2  32524  cvmlift2lem12  32556  cvmliftpht  32560  nocvxminlem  33242  finminlem  33661  onint1  33792  finxpreclem4  34669  heicant  34921  itg2addnc  34940  ftc1anclem7  34967  ftc1anc  34969  prdsbnd2  35067  lkrlss  36225  pclvalN  37020  dian0  38169  docaclN  38254  dicn0  38322  dihglblem5  38428  dihglb2  38472  doch2val2  38494  dochocss  38496  lclkr  38663  lclkrs  38669  lcfr  38715  qsalrel  39118  nacsfix  39302  mzpcln0  39318  rencldnfilem  39410  fnwe2lem2  39644  kelac1  39656  harn0  39695  hbtlem2  39717  gneispa  40473  scottrankd  40577  ubelsupr  41270  suprnmpt  41423  disjinfi  41447  suprubrnmpt2  41517  suprubrnmpt  41518  ssfiunibd  41569  allbutfi  41658  allbutfiinf  41687  uzn0d  41692  uzublem  41697  climinf  41880  limclr  41929  climinf2lem  41980  limsupubuzlem  41986  liminflelimsupuz  42059  cnrefiisplem  42103  ioodvbdlimc1lem1  42209  ioodvbdlimc1  42211  ioodvbdlimc2  42213  stoweidlem36  42315  fourierdlem20  42406  fourierdlem25  42411  fourierdlem31  42417  fourierdlem37  42423  fourierdlem46  42431  fourierdlem52  42437  fourierdlem54  42439  fouriercn  42511  elaa2lem  42512  salgenval  42600  salgenn0  42608  sge0isum  42703  sge0reuzb  42724  ovnlerp  42838  ovnf  42839  hsphoidmvle2  42861  hsphoidmvle  42862  hoiprodp1  42864  hoidmv1lelem1  42867  hoidmv1lelem3  42869  hoidmv1le  42870  hoidifhspdmvle  42896  hspmbllem1  42902  hspmbllem3  42904  ovnovollem2  42933  smflimlem1  43041  smfsuplem1  43079  smfsuplem3  43081  smflimsuplem5  43092  smflimsuplem7  43094  preimafvn0  43534  lincolss  44483