Theorem ne0d 4336

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

Syntax hints:   → wi 4   ∈ wcel 2107   ≠ wne 2941  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-dif 3952  df-nul 4324

This theorem is referenced by:  snnzg  4779  prnzg  4783  exss  5464  isofrlem  7337  fvmpocurryd  8256  onnseq  8344  oeoalem  8596  oeoelem  8598  oeeui  8602  nnawordex  8637  omxpenlem  9073  frfi  9288  supgtoreq  9465  infltoreq  9497  cantnfp1lem2  9674  cantnfp1lem3  9675  oemapvali  9679  cantnflem1a  9680  cantnflem1d  9683  cantnflem1  9684  epfrs  9726  dfac9  10131  axdc3lem4  10448  intwun  10730  r1limwun  10731  gruina  10813  grur1a  10814  mulclpi  10888  indpi  10902  supsrlem  11106  axpre-sup  11164  supfirege  12201  uzn0  12839  suprzub  12923  fzn0  13515  flval3  13780  icopnfsup  13830  hashelne0d  14328  dfrtrcl2  15009  01sqrexlem3  15191  isercolllem2  15612  isercolllem3  15613  climsup  15616  mertenslem2  15831  gcdcllem1  16440  pclem  16771  prmreclem1  16849  4sqlem13  16890  vdwmc2  16912  vdwlem6  16919  vdwnnlem3  16930  prmgaplem3  16986  prmgaplem4  16987  mrcflem  17550  mrcval  17554  iscatd2  17625  mndbn0  18641  grpbn0  18851  issubgrpd2  19022  issubg4  19025  subgint  19030  nmzsubg  19045  cycsubgcl  19083  ghmpreima  19114  gastacl  19173  sylow1lem5  19470  pgpssslw  19482  sylow2alem2  19486  sylow2blem3  19490  fislw  19493  sylow3lem4  19498  torsubg  19722  oddvdssubg  19723  iscygd  19755  iscygodd  19756  dprdsubg  19894  ablfac1eu  19943  simpgnideld  19969  01eq0ring  20305  cntzsubr  20353  imadrhmcl  20413  primefld  20421  primefld0cl  20422  primefld1cl  20423  islss4  20573  lss1d  20574  lssintcl  20575  lspsolvlem  20755  lbsextlem1  20771  lidlsubg  20838  dflidl2lem  20842  abvn0b  20920  zringlpirlem1  21032  ocvlss  21225  lmiclbs  21392  lmisfree  21397  psrbas  21497  mplsubglem  21558  mplind  21631  mhpsubg  21696  mat1ric  21989  dmatsgrp  22001  scmatsgrp  22021  scmatsgrp1  22024  scmatlss  22027  scmatric  22039  cpmatsubgpmat  22222  matcpmric  22261  pmmpric  22325  clscld  22551  2ndcdisj  22960  dfac14lem  23121  opnfbas  23346  isfil2  23360  filn0  23366  filssufilg  23415  rnelfmlem  23456  flimfnfcls  23532  ptcmplem2  23557  clssubg  23613  tgpconncomp  23617  tsmsfbas  23632  ustfilxp  23717  ustne0  23718  xbln0  23920  bln0  23921  metustfbas  24066  metustbl  24075  nrgdomn  24188  icccmplem2  24339  icccmplem3  24340  reconnlem2  24343  phtpcer  24511  reparpht  24514  phtpcco2  24515  pcohtpy  24536  pcorevlem  24542  isclmp  24613  iscmet3lem2  24809  bcthlem4  24844  minveclem3b  24945  ivthlem2  24969  ivthlem3  24970  evthicc  24976  ovollb2  25006  ovolunlem1a  25013  ovolunlem1  25014  ovoliunlem1  25019  ovoliun2  25023  ioombl1lem4  25078  uniioombllem1  25098  uniioombllem2  25100  uniioombllem6  25105  mbfsup  25181  mbfinf  25182  mbflimsup  25183  itg2monolem1  25268  itg2mono  25271  ulm0  25903  pilem2  25964  pilem3  25965  ftalem3  26579  ftalem4  26580  ftalem5  26581  dchrabs  26763  pntlem3  27112  nocvxminlem  27279  tglnne0  27891  axlowdim1  28217  nvo00  30014  nmorepnf  30021  minvecolem1  30127  submomnd  32228  cycpmco2lem5  32289  primefldchr  32399  fldgensdrg  32404  suborng  32433  nsgqusf1olem1  32524  intlidl  32536  rhmpreimaidl  32537  idlinsubrg  32549  rhmimaidl  32550  ssmxidl  32590  ply1degltlss  32667  ordtconnlem1  32904  rrhre  33001  sigagenval  33138  oddpwdc  33353  bnj1177  34017  bnj1523  34082  erdszelem8  34189  txsconnlem  34231  cvxsconn  34234  cvmsss2  34265  cvmliftmolem2  34273  cvmlift2lem12  34305  cvmliftpht  34309  finminlem  35203  onint1  35334  finxpreclem4  36275  heicant  36523  itg2addnc  36542  ftc1anclem7  36567  ftc1anc  36569  prdsbnd2  36663  lkrlss  37965  pclvalN  38761  dian0  39910  docaclN  39995  dicn0  40063  dihglblem5  40169  dihglb2  40213  doch2val2  40235  dochocss  40237  lclkr  40404  lclkrs  40410  lcfr  40456  qsalrel  41062  nacsfix  41450  mzpcln0  41466  rencldnfilem  41558  fnwe2lem2  41793  kelac1  41805  harn0  41844  hbtlem2  41866  naddwordnexlem4  42152  omltoe  42158  gneispa  42881  scottrankd  43007  ubelsupr  43704  suprnmpt  43870  disjinfi  43891  suprubrnmpt2  43956  suprubrnmpt  43957  ssfiunibd  44019  allbutfi  44103  allbutfiinf  44130  uzn0d  44135  uzublem  44140  climinf  44322  limclr  44371  climinf2lem  44422  limsupubuzlem  44428  liminflelimsupuz  44501  cnrefiisplem  44545  ioodvbdlimc1lem1  44647  ioodvbdlimc1  44649  ioodvbdlimc2  44651  stoweidlem36  44752  fourierdlem20  44843  fourierdlem25  44848  fourierdlem31  44854  fourierdlem37  44860  fourierdlem46  44868  fourierdlem52  44874  fourierdlem54  44876  fouriercn  44948  elaa2lem  44949  salgenval  45037  salgenn0  45047  sge0isum  45143  sge0reuzb  45164  ovnlerp  45278  ovnf  45279  hsphoidmvle2  45301  hsphoidmvle  45302  hoiprodp1  45304  hoidmv1lelem1  45307  hoidmv1lelem3  45309  hoidmv1le  45310  hoidifhspdmvle  45336  hspmbllem1  45342  hspmbllem3  45344  ovnovollem2  45373  smflimlem1  45487  smfsuplem1  45527  smfsuplem3  45529  smflimsuplem5  45540  smflimsuplem7  45542  preimafvn0  46048  cntzsubrng  46746  dflidl2rng  46750  lincolss  47115  fvconstr2  47524  catprs  47631