Theorem ne0d 4304

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

Syntax hints:   → wi 4   ∈ wcel 2113   ≠ wne 3019  ∅c0 4294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-ne 3020  df-dif 3942  df-nul 4295

This theorem is referenced by:  snnzg  4713  prnzg  4716  exss  5358  isofrlem  7096  fvmpocurryd  7940  onnseq  7984  oeoalem  8225  oeoelem  8227  oeeui  8231  nnawordex  8266  omxpenlem  8621  frfi  8766  supgtoreq  8937  infltoreq  8969  cantnfp1lem2  9145  cantnfp1lem3  9146  oemapvali  9150  cantnflem1a  9151  cantnflem1d  9154  cantnflem1  9155  epfrs  9176  dfac9  9565  axdc3lem4  9878  intwun  10160  r1limwun  10161  gruina  10243  grur1a  10244  mulclpi  10318  indpi  10332  supsrlem  10536  axpre-sup  10594  supfirege  11630  uzn0  12263  suprzub  12342  fzn0  12924  flval3  13188  icopnfsup  13236  hashelne0d  13732  dfrtrcl2  14424  sqrlem3  14607  isercolllem2  15025  isercolllem3  15026  climsup  15029  mertenslem2  15244  gcdcllem1  15851  pclem  16178  prmreclem1  16255  4sqlem13  16296  vdwmc2  16318  vdwlem6  16325  vdwnnlem3  16336  prmgaplem3  16392  prmgaplem4  16393  mrcflem  16880  mrcval  16884  iscatd2  16955  mndbn0  17930  grpbn0  18135  issubgrpd2  18298  issubg4  18301  subgint  18306  nmzsubg  18320  cycsubgcl  18352  ghmpreima  18383  gastacl  18442  sylow1lem5  18730  pgpssslw  18742  sylow2alem2  18746  sylow2blem3  18750  fislw  18753  sylow3lem4  18758  torsubg  18977  oddvdssubg  18978  iscygd  19009  iscygodd  19010  dprdsubg  19149  ablfac1eu  19198  simpgnideld  19224  cntzsubr  19571  primefld  19587  primefld0cl  19588  primefld1cl  19589  islss4  19737  lss1d  19738  lssintcl  19739  lspsolvlem  19917  lbsextlem1  19933  lidlsubg  19991  abvn0b  20078  psrbas  20161  mplsubglem  20217  mplind  20285  mhpsubg  20343  zringlpirlem1  20634  ocvlss  20819  lmiclbs  20984  lmisfree  20989  mat1ric  21099  dmatsgrp  21111  scmatsgrp  21131  scmatsgrp1  21134  scmatlss  21137  scmatric  21149  cpmatsubgpmat  21331  matcpmric  21370  pmmpric  21434  clscld  21658  2ndcdisj  22067  dfac14lem  22228  opnfbas  22453  isfil2  22467  filn0  22473  filssufilg  22522  rnelfmlem  22563  flimfnfcls  22639  ptcmplem2  22664  clssubg  22720  tgpconncomp  22724  tsmsfbas  22739  ustfilxp  22824  ustne0  22825  xbln0  23027  bln0  23028  metustfbas  23170  metustbl  23179  nrgdomn  23283  icccmplem2  23434  icccmplem3  23435  reconnlem2  23438  phtpcer  23602  reparpht  23605  phtpcco2  23606  pcohtpy  23627  pcorevlem  23633  isclmp  23704  iscmet3lem2  23898  bcthlem4  23933  minveclem3b  24034  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  24982  pilem2  25043  pilem3  25044  ftalem3  25655  ftalem4  25656  ftalem5  25657  dchrabs  25839  pntlem3  26188  tglnne0  26429  axlowdim1  26748  nvo00  28541  nmorepnf  28548  minvecolem1  28654  submomnd  30715  cycpmco2lem5  30776  primefldchr  30871  suborng  30892  ssmxidl  30983  ordtconnlem1  31171  rrhre  31266  sigagenval  31403  oddpwdc  31616  bnj1177  32282  bnj1523  32347  erdszelem8  32449  txsconnlem  32491  cvxsconn  32494  cvmsss2  32525  cvmliftmolem2  32533  cvmlift2lem12  32565  cvmliftpht  32569  nocvxminlem  33251  finminlem  33670  onint1  33801  finxpreclem4  34679  heicant  34931  itg2addnc  34950  ftc1anclem7  34977  ftc1anc  34979  prdsbnd2  35077  lkrlss  36235  pclvalN  37030  dian0  38179  docaclN  38264  dicn0  38332  dihglblem5  38438  dihglb2  38482  doch2val2  38504  dochocss  38506  lclkr  38673  lclkrs  38679  lcfr  38725  qsalrel  39131  nacsfix  39315  mzpcln0  39331  rencldnfilem  39423  fnwe2lem2  39657  kelac1  39669  harn0  39708  hbtlem2  39730  gneispa  40486  scottrankd  40590  ubelsupr  41283  suprnmpt  41436  disjinfi  41460  suprubrnmpt2  41530  suprubrnmpt  41531  ssfiunibd  41582  allbutfi  41671  allbutfiinf  41700  uzn0d  41705  uzublem  41710  climinf  41893  limclr  41942  climinf2lem  41993  limsupubuzlem  41999  liminflelimsupuz  42072  cnrefiisplem  42116  ioodvbdlimc1lem1  42222  ioodvbdlimc1  42224  ioodvbdlimc2  42226  stoweidlem36  42328  fourierdlem20  42419  fourierdlem25  42424  fourierdlem31  42430  fourierdlem37  42436  fourierdlem46  42444  fourierdlem52  42450  fourierdlem54  42452  fouriercn  42524  elaa2lem  42525  salgenval  42613  salgenn0  42621  sge0isum  42716  sge0reuzb  42737  ovnlerp  42851  ovnf  42852  hsphoidmvle2  42874  hsphoidmvle  42875  hoiprodp1  42877  hoidmv1lelem1  42880  hoidmv1lelem3  42882  hoidmv1le  42883  hoidifhspdmvle  42909  hspmbllem1  42915  hspmbllem3  42917  ovnovollem2  42946  smflimlem1  43054  smfsuplem1  43092  smfsuplem3  43094  smflimsuplem5  43105  smflimsuplem7  43107  preimafvn0  43547  lincolss  44496