Theorem ne0d 4251

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

Syntax hints:   → wi 4   ∈ wcel 2111   ≠ wne 2987  ∅c0 4243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-dif 3884  df-nul 4244

This theorem is referenced by:  snnzg  4670  prnzg  4674  exss  5320  isofrlem  7072  fvmpocurryd  7920  onnseq  7964  oeoalem  8205  oeoelem  8207  oeeui  8211  nnawordex  8246  omxpenlem  8601  frfi  8747  supgtoreq  8918  infltoreq  8950  cantnfp1lem2  9126  cantnfp1lem3  9127  oemapvali  9131  cantnflem1a  9132  cantnflem1d  9135  cantnflem1  9136  epfrs  9157  dfac9  9547  axdc3lem4  9864  intwun  10146  r1limwun  10147  gruina  10229  grur1a  10230  mulclpi  10304  indpi  10318  supsrlem  10522  axpre-sup  10580  supfirege  11614  uzn0  12248  suprzub  12327  fzn0  12916  flval3  13180  icopnfsup  13228  hashelne0d  13725  dfrtrcl2  14413  sqrlem3  14596  isercolllem2  15014  isercolllem3  15015  climsup  15018  mertenslem2  15233  gcdcllem1  15838  pclem  16165  prmreclem1  16242  4sqlem13  16283  vdwmc2  16305  vdwlem6  16312  vdwnnlem3  16323  prmgaplem3  16379  prmgaplem4  16380  mrcflem  16869  mrcval  16873  iscatd2  16944  mndbn0  17919  grpbn0  18124  issubgrpd2  18287  issubg4  18290  subgint  18295  nmzsubg  18309  cycsubgcl  18341  ghmpreima  18372  gastacl  18431  sylow1lem5  18719  pgpssslw  18731  sylow2alem2  18735  sylow2blem3  18739  fislw  18742  sylow3lem4  18747  torsubg  18967  oddvdssubg  18968  iscygd  18999  iscygodd  19000  dprdsubg  19139  ablfac1eu  19188  simpgnideld  19214  cntzsubr  19561  primefld  19577  primefld0cl  19578  primefld1cl  19579  islss4  19727  lss1d  19728  lssintcl  19729  lspsolvlem  19907  lbsextlem1  19923  lidlsubg  19981  abvn0b  20068  zringlpirlem1  20177  ocvlss  20361  lmiclbs  20526  lmisfree  20531  psrbas  20616  mplsubglem  20672  mplind  20741  mhpsubg  20801  mat1ric  21092  dmatsgrp  21104  scmatsgrp  21124  scmatsgrp1  21127  scmatlss  21130  scmatric  21142  cpmatsubgpmat  21325  matcpmric  21364  pmmpric  21428  clscld  21652  2ndcdisj  22061  dfac14lem  22222  opnfbas  22447  isfil2  22461  filn0  22467  filssufilg  22516  rnelfmlem  22557  flimfnfcls  22633  ptcmplem2  22658  clssubg  22714  tgpconncomp  22718  tsmsfbas  22733  ustfilxp  22818  ustne0  22819  xbln0  23021  bln0  23022  metustfbas  23164  metustbl  23173  nrgdomn  23277  icccmplem2  23428  icccmplem3  23429  reconnlem2  23432  phtpcer  23600  reparpht  23603  phtpcco2  23604  pcohtpy  23625  pcorevlem  23631  isclmp  23702  iscmet3lem2  23896  bcthlem4  23931  minveclem3b  24032  ivthlem2  24056  ivthlem3  24057  evthicc  24063  ovollb2  24093  ovolunlem1a  24100  ovolunlem1  24101  ovoliunlem1  24106  ovoliun2  24110  ioombl1lem4  24165  uniioombllem1  24185  uniioombllem2  24187  uniioombllem6  24192  mbfsup  24268  mbfinf  24269  mbflimsup  24270  itg2monolem1  24354  itg2mono  24357  ulm0  24986  pilem2  25047  pilem3  25048  ftalem3  25660  ftalem4  25661  ftalem5  25662  dchrabs  25844  pntlem3  26193  tglnne0  26434  axlowdim1  26753  nvo00  28544  nmorepnf  28551  minvecolem1  28657  submomnd  30761  cycpmco2lem5  30822  primefldchr  30918  suborng  30939  intlidl  31010  rhmpreimaidl  31011  idlinsubrg  31016  rhmimaidl  31017  ssmxidl  31050  ordtconnlem1  31277  rrhre  31372  sigagenval  31509  oddpwdc  31722  bnj1177  32388  bnj1523  32453  erdszelem8  32558  txsconnlem  32600  cvxsconn  32603  cvmsss2  32634  cvmliftmolem2  32642  cvmlift2lem12  32674  cvmliftpht  32678  nocvxminlem  33360  finminlem  33779  onint1  33910  finxpreclem4  34811  heicant  35092  itg2addnc  35111  ftc1anclem7  35136  ftc1anc  35138  prdsbnd2  35233  lkrlss  36391  pclvalN  37186  dian0  38335  docaclN  38420  dicn0  38488  dihglblem5  38594  dihglb2  38638  doch2val2  38660  dochocss  38662  lclkr  38829  lclkrs  38835  lcfr  38881  qsalrel  39420  nacsfix  39653  mzpcln0  39669  rencldnfilem  39761  fnwe2lem2  39995  kelac1  40007  harn0  40046  hbtlem2  40068  gneispa  40833  scottrankd  40956  ubelsupr  41649  suprnmpt  41798  disjinfi  41820  suprubrnmpt2  41890  suprubrnmpt  41891  ssfiunibd  41941  allbutfi  42029  allbutfiinf  42057  uzn0d  42062  uzublem  42067  climinf  42248  limclr  42297  climinf2lem  42348  limsupubuzlem  42354  liminflelimsupuz  42427  cnrefiisplem  42471  ioodvbdlimc1lem1  42573  ioodvbdlimc1  42575  ioodvbdlimc2  42577  stoweidlem36  42678  fourierdlem20  42769  fourierdlem25  42774  fourierdlem31  42780  fourierdlem37  42786  fourierdlem46  42794  fourierdlem52  42800  fourierdlem54  42802  fouriercn  42874  elaa2lem  42875  salgenval  42963  salgenn0  42971  sge0isum  43066  sge0reuzb  43087  ovnlerp  43201  ovnf  43202  hsphoidmvle2  43224  hsphoidmvle  43225  hoiprodp1  43227  hoidmv1lelem1  43230  hoidmv1lelem3  43232  hoidmv1le  43233  hoidifhspdmvle  43259  hspmbllem1  43265  hspmbllem3  43267  ovnovollem2  43296  smflimlem1  43404  smfsuplem1  43442  smfsuplem3  43444  smflimsuplem5  43455  smflimsuplem7  43457  preimafvn0  43897  lincolss  44843