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

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

Syntax hints:   → wi 4   ∈ wcel 2143   ≠ wne 2958  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-dif 3909  df-nul 4288

This theorem is referenced by:  snnzg  4741  prnzg  4745  eqsnd  4797  exss  5446  isofrlem  7340  peano3  7888  fvmpocurryd  8268  onnseq  8332  oeoalem  8583  oeoelem  8585  oeeui  8589  nnawordex  8624  omxpenlem  9067  frfi  9246  supgtoreq  9432  infltoreq  9465  cantnfp1lem2  9649  cantnfp1lem3  9650  oemapvali  9654  cantnflem1a  9655  cantnflem1d  9658  cantnflem1  9659  epfrs  9701  scottrankd  9875  dfac9  10121  axdc3lem4  10438  intwun  10721  r1limwun  10722  gruina  10804  grur1a  10805  mulclpi  10879  indpi  10893  supsrlem  11097  axpre-sup  11155  supfirege  12203  uzn0  12880  suprzub  12964  fzn0  13567  flval3  13850  icopnfsup  13900  hashelne0d  14406  dfrtrcl2  15101  01sqrexlem3  15297  isercolllem2  15719  isercolllem3  15720  climsup  15723  mertenslem2  15941  gcdcllem1  16558  pclem  16899  prmreclem1  16977  4sqlem13  17018  vdwmc2  17040  vdwlem6  17047  vdwnnlem3  17058  prmgaplem3  17114  prmgaplem4  17115  mrcflem  17663  mrcval  17667  iscatd2  17738  chnub  18679  mndbn0  18809  grpbn0  19034  issubgrpd2  19210  issubg4  19213  subgint  19218  nmzsubg  19232  cycsubgcl  19278  ghmpreima  19309  gastacl  19380  sylow1lem5  19673  pgpssslw  19685  sylow2alem2  19689  sylow2blem3  19693  fislw  19696  sylow3lem4  19701  torsubg  19925  oddvdssubg  19926  iscygd  19958  iscygodd  19959  dprdsubg  20097  ablfac1eu  20146  simpgnideld  20172  submomnd  20203  01eq0ring  20615  cntzsubrng  20653  cntzsubr  20692  imadrhmcl  20881  primefld  20889  primefld0cl  20890  primefld1cl  20891  abvn0b  20920  suborng  20960  islss4  21064  lss1d  21065  lssintcl  21066  lspsolvlem  21247  lbsextlem1  21263  dflidl2rng  21324  lidlsubg  21329  lidlunin0  21342  rhmpreimaidl  21397  ssdifidl  21466  ssdifidlprm  21467  zringlpirlem1  21593  ocvlss  21803  lmiclbs  21968  lmisfree  21973  psrbas  22065  mplsubglem  22129  mplind  22202  mhpsubg  22297  mat1ric  22625  dmatsgrp  22637  scmatsgrp  22657  scmatsgrp1  22660  scmatlss  22663  scmatric  22675  cpmatsubgpmat  22858  matcpmric  22897  pmmpric  22961  clscld  23185  2ndcdisj  23594  dfac14lem  23755  opnfbas  23980  isfil2  23994  filn0  24000  filssufilg  24049  rnelfmlem  24090  flimfnfcls  24166  ptcmplem2  24191  clssubg  24247  tgpconncomp  24251  tsmsfbas  24266  ustfilxp  24351  ustne0  24352  xbln0  24552  bln0  24553  metustfbas  24695  metustbl  24704  nrgdomn  24809  icccmplem2  24962  icccmplem3  24963  reconnlem2  24966  phtpcer  25135  reparpht  25138  phtpcco2  25139  pcohtpy  25160  pcorevlem  25166  isclmp  25237  iscmet3lem2  25432  bcthlem4  25467  minveclem3b  25568  ivthlem2  25592  ivthlem3  25593  evthicc  25599  ovollb2  25629  ovolunlem1a  25636  ovolunlem1  25637  ovoliunlem1  25642  ovoliun2  25646  ioombl1lem4  25701  uniioombllem1  25721  uniioombllem2  25723  uniioombllem6  25728  mbfsup  25804  mbfinf  25805  mbflimsup  25806  itg2monolem1  25890  itg2mono  25893  ulm0  26535  pilem2  26596  pilem3  26597  ftalem3  27220  ftalem4  27221  ftalem5  27222  dchrabs  27405  pntlem3  27754  nocvxminlem  27928  bdayfinbndlem1  28641  tglnne0  28895  tglnpt4  28909  prlngmolem1  29183  prlngmolem2  29184  prlngmo2  29187  prlngpln4  29189  prlngsymquadlem  29194  quadcgrprlng  29197  axlowdim1  29290  nvo00  31094  nmorepnf  31101  minvecolem1  31207  wrdpmtrlast  33394  cycpmco2lem5  33431  elrgspnlem1  33543  primefldchr  33603  fldgensdrg  33616  nsgqusf1olem1  33703  intlidl  33709  idlinsubrg  33720  rhmimaidl  33721  ssmxidl  33738  dflringlem2  33766  pidufd  33814  1arithufdlem1  33815  ply1dg1rtn0  33852  ply1degltlss  33867  exsslsb  33968  constrsdrg  34146  ordtconnlem1  34295  rrhre  34392  sigagenval  34511  oddpwdc  34725  bnj1177  35375  bnj1523  35440  rankfilimbi  35476  erdszelem8  35671  txsconnlem  35713  cvxsconn  35716  cvmsss2  35747  cvmliftmolem2  35755  cvmlift2lem12  35787  cvmliftpht  35791  finminlem  36810  onint1  36941  weiunlem  36955  weiunfr  36959  finxpreclem4  38021  heicant  38287  itg2addnc  38306  ftc1anclem7  38331  ftc1anc  38333  prdsbnd2  38427  lkrlss  39850  pclvalN  40645  dian0  41794  docaclN  41879  dicn0  41947  dihglblem5  42053  dihglb2  42097  doch2val2  42119  dochocss  42121  lclkr  42288  lclkrs  42294  lcfr  42340  aks6d1c6lem3  42920  unitscyglem2  42944  qsalrel  42990  nacsfix  43426  mzpcln0  43442  rencldnfilem  43530  fnwe2lem2  43761  kelac1  43773  harn0  43812  hbtlem2  43834  naddwordnexlem4  44111  omltoe  44116  gneispa  44839  imo72b2lem0  44874  relpfrlem  45645  ubelsupr  45723  suprnmpt  45875  disjinfi  45893  suprubrnmpt2  45950  suprubrnmpt  45951  ssfiunibd  46011  allbutfi  46091  allbutfiinf  46117  uzn0d  46122  uzublem  46127  climinf  46305  limclr  46352  climinf2lem  46403  limsupubuzlem  46409  liminflelimsupuz  46482  cnrefiisplem  46526  ioodvbdlimc1lem1  46628  ioodvbdlimc1  46630  ioodvbdlimc2  46632  stoweidlem36  46733  fourierdlem20  46824  fourierdlem25  46829  fourierdlem31  46835  fourierdlem37  46841  fourierdlem46  46849  fourierdlem48  46851  fourierdlem49  46852  fourierdlem52  46855  fourierdlem54  46857  fouriercn  46929  elaa2lem  46930  salgenval  47018  salgenn0  47028  sge0isum  47124  sge0reuzb  47145  ovnlerp  47259  ovnf  47260  hsphoidmvle2  47282  hsphoidmvle  47283  hoiprodp1  47285  hoidmv1lelem1  47288  hoidmv1lelem3  47290  hoidmv1le  47291  hoidifhspdmvle  47317  hspmbllem1  47323  hspmbllem3  47325  ovnovollem2  47354  smflimlem1  47468  smfsuplem1  47508  smfsuplem3  47510  smflimsuplem5  47521  smflimsuplem7  47523  preimafvn0  48112  lincolss  49197  fvconstr2  49625  catprs  49772  discsubc  49825  iinfconstbas  49827  eloppf  49894  eloppf2  49895  oppcup3  49970  oppcthinendcALT  50202  termcterm3  50276  termcciso  50277  idfudiag1bas  50285  idfudiag1  50286