Theorem ne0d 4294

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

Syntax hints:   → wi 4   ∈ wcel 2141   ≠ wne 2956  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-dif 3907  df-nul 4286

This theorem is referenced by:  snnzg  4732  prnzg  4736  eqsnd  4787  exss  5429  isofrlem  7320  peano3  7867  fvmpocurryd  8246  onnseq  8310  oeoalem  8561  oeoelem  8563  oeeui  8567  nnawordex  8602  omxpenlem  9046  frfi  9225  supgtoreq  9414  infltoreq  9447  cantnfp1lem2  9631  cantnfp1lem3  9632  oemapvali  9636  cantnflem1a  9637  cantnflem1d  9640  cantnflem1  9641  epfrs  9683  dfac9  10090  axdc3lem4  10407  intwun  10690  r1limwun  10691  gruina  10773  grur1a  10774  mulclpi  10848  indpi  10862  supsrlem  11066  axpre-sup  11124  supfirege  12176  uzn0  12853  suprzub  12937  fzn0  13540  flval3  13822  icopnfsup  13872  hashelne0d  14378  dfrtrcl2  15072  01sqrexlem3  15254  isercolllem2  15676  isercolllem3  15677  climsup  15680  mertenslem2  15898  gcdcllem1  16516  pclem  16857  prmreclem1  16935  4sqlem13  16976  vdwmc2  16998  vdwlem6  17005  vdwnnlem3  17016  prmgaplem3  17072  prmgaplem4  17073  mrcflem  17621  mrcval  17625  iscatd2  17696  chnub  18637  mndbn0  18767  grpbn0  18991  issubgrpd2  19167  issubg4  19170  subgint  19175  nmzsubg  19189  cycsubgcl  19230  ghmpreima  19261  gastacl  19332  sylow1lem5  19625  pgpssslw  19637  sylow2alem2  19641  sylow2blem3  19645  fislw  19648  sylow3lem4  19653  torsubg  19877  oddvdssubg  19878  iscygd  19910  iscygodd  19911  dprdsubg  20049  ablfac1eu  20098  simpgnideld  20124  submomnd  20155  01eq0ring  20559  cntzsubrng  20596  cntzsubr  20635  imadrhmcl  20826  primefld  20834  primefld0cl  20835  primefld1cl  20836  abvn0b  20865  suborng  20905  islss4  21009  lss1d  21010  lssintcl  21011  lspsolvlem  21192  lbsextlem1  21208  dflidl2rng  21268  lidlsubg  21273  rhmpreimaidl  21327  zringlpirlem1  21494  ocvlss  21704  lmiclbs  21869  lmisfree  21874  psrbas  21966  mplsubglem  22030  mplind  22103  mhpsubg  22198  mat1ric  22527  dmatsgrp  22539  scmatsgrp  22559  scmatsgrp1  22562  scmatlss  22565  scmatric  22577  cpmatsubgpmat  22760  matcpmric  22799  pmmpric  22863  clscld  23087  2ndcdisj  23496  dfac14lem  23657  opnfbas  23882  isfil2  23896  filn0  23902  filssufilg  23951  rnelfmlem  23992  flimfnfcls  24068  ptcmplem2  24093  clssubg  24149  tgpconncomp  24153  tsmsfbas  24168  ustfilxp  24253  ustne0  24254  xbln0  24454  bln0  24455  metustfbas  24597  metustbl  24606  nrgdomn  24711  icccmplem2  24864  icccmplem3  24865  reconnlem2  24868  phtpcer  25037  reparpht  25040  phtpcco2  25041  pcohtpy  25062  pcorevlem  25068  isclmp  25139  iscmet3lem2  25334  bcthlem4  25369  minveclem3b  25470  ivthlem2  25494  ivthlem3  25495  evthicc  25501  ovollb2  25531  ovolunlem1a  25538  ovolunlem1  25539  ovoliunlem1  25544  ovoliun2  25548  ioombl1lem4  25603  uniioombllem1  25623  uniioombllem2  25625  uniioombllem6  25630  mbfsup  25706  mbfinf  25707  mbflimsup  25708  itg2monolem1  25792  itg2mono  25795  ulm0  26431  pilem2  26492  pilem3  26493  ftalem3  27116  ftalem4  27117  ftalem5  27118  dchrabs  27301  pntlem3  27650  nocvxminlem  27824  bdayfinbndlem1  28537  tglnne0  28786  axlowdim1  29106  nvo00  30910  nmorepnf  30917  minvecolem1  31023  wrdpmtrlast  33234  cycpmco2lem5  33271  elrgspnlem1  33384  primefldchr  33449  fldgensdrg  33462  nsgqusf1olem1  33560  intlidl  33567  idlinsubrg  33578  rhmimaidl  33579  ssdifidl  33605  ssdifidlprm  33606  ssmxidl  33623  dflringlem2  33652  pidufd  33700  1arithufdlem1  33701  ply1dg1rtn0  33738  ply1degltlss  33753  exsslsb  33855  constrsdrg  34033  ordtconnlem1  34182  rrhre  34279  sigagenval  34398  oddpwdc  34612  bnj1177  35265  bnj1523  35330  rankfilimbi  35361  erdszelem8  35512  txsconnlem  35554  cvxsconn  35557  cvmsss2  35588  cvmliftmolem2  35596  cvmlift2lem12  35628  cvmliftpht  35632  finminlem  36642  onint1  36773  weiunlem  36787  weiunfr  36791  finxpreclem4  37852  heicant  38118  itg2addnc  38137  ftc1anclem7  38162  ftc1anc  38164  prdsbnd2  38258  lkrlss  39683  pclvalN  40478  dian0  41627  docaclN  41712  dicn0  41780  dihglblem5  41886  dihglb2  41930  doch2val2  41952  dochocss  41954  lclkr  42121  lclkrs  42127  lcfr  42173  aks6d1c6lem3  42753  unitscyglem2  42777  qsalrel  42821  nacsfix  43257  mzpcln0  43273  rencldnfilem  43361  fnwe2lem2  43592  kelac1  43604  harn0  43643  hbtlem2  43665  naddwordnexlem4  43942  omltoe  43947  gneispa  44670  imo72b2lem0  44705  scottrankd  44788  relpfrlem  45493  ubelsupr  45564  suprnmpt  45716  disjinfi  45734  suprubrnmpt2  45791  suprubrnmpt  45792  ssfiunibd  45852  allbutfi  45932  allbutfiinf  45958  uzn0d  45963  uzublem  45968  climinf  46146  limclr  46193  climinf2lem  46244  limsupubuzlem  46250  liminflelimsupuz  46323  cnrefiisplem  46367  ioodvbdlimc1lem1  46469  ioodvbdlimc1  46471  ioodvbdlimc2  46473  stoweidlem36  46574  fourierdlem20  46665  fourierdlem25  46670  fourierdlem31  46676  fourierdlem37  46682  fourierdlem46  46690  fourierdlem48  46692  fourierdlem49  46693  fourierdlem52  46696  fourierdlem54  46698  fouriercn  46770  elaa2lem  46771  salgenval  46859  salgenn0  46869  sge0isum  46965  sge0reuzb  46986  ovnlerp  47100  ovnf  47101  hsphoidmvle2  47123  hsphoidmvle  47124  hoiprodp1  47126  hoidmv1lelem1  47129  hoidmv1lelem3  47131  hoidmv1le  47132  hoidifhspdmvle  47158  hspmbllem1  47164  hspmbllem3  47166  ovnovollem2  47195  smflimlem1  47309  smfsuplem1  47349  smfsuplem3  47351  smflimsuplem5  47362  smflimsuplem7  47364  preimafvn0  47950  lincolss  49020  fvconstr2  49449  catprs  49596  discsubc  49649  iinfconstbas  49651  eloppf  49718  eloppf2  49719  oppcup3  49794  oppcthinendcALT  50026  termcterm3  50100  termcciso  50101  idfudiag1bas  50109  idfudiag1  50110