Theorem ne0d 4291

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

Syntax hints:   → wi 4   ∈ wcel 2113   ≠ wne 2929  ∅c0 4282

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-dif 3901  df-nul 4283

This theorem is referenced by:  snnzg  4728  prnzg  4732  eqsnd  4783  exss  5408  isofrlem  7282  fvmpocurryd  8209  onnseq  8272  oeoalem  8519  oeoelem  8521  oeeui  8525  nnawordex  8560  omxpenlem  9000  frfi  9178  supgtoreq  9364  infltoreq  9397  cantnfp1lem2  9578  cantnfp1lem3  9579  oemapvali  9583  cantnflem1a  9584  cantnflem1d  9587  cantnflem1  9588  epfrs  9630  dfac9  10037  axdc3lem4  10353  intwun  10635  r1limwun  10636  gruina  10718  grur1a  10719  mulclpi  10793  indpi  10807  supsrlem  11011  axpre-sup  11069  supfirege  12118  uzn0  12757  suprzub  12841  fzn0  13442  flval3  13723  icopnfsup  13773  hashelne0d  14279  dfrtrcl2  14973  01sqrexlem3  15155  isercolllem2  15577  isercolllem3  15578  climsup  15581  mertenslem2  15796  gcdcllem1  16414  pclem  16754  prmreclem1  16832  4sqlem13  16873  vdwmc2  16895  vdwlem6  16902  vdwnnlem3  16913  prmgaplem3  16969  prmgaplem4  16970  mrcflem  17516  mrcval  17520  iscatd2  17591  chnub  18532  mndbn0  18662  grpbn0  18883  issubgrpd2  19059  issubg4  19062  subgint  19067  nmzsubg  19081  cycsubgcl  19122  ghmpreima  19154  gastacl  19225  sylow1lem5  19518  pgpssslw  19530  sylow2alem2  19534  sylow2blem3  19538  fislw  19541  sylow3lem4  19546  torsubg  19770  oddvdssubg  19771  iscygd  19803  iscygodd  19804  dprdsubg  19942  ablfac1eu  19991  simpgnideld  20017  submomnd  20048  01eq0ring  20449  cntzsubrng  20486  cntzsubr  20525  imadrhmcl  20716  primefld  20724  primefld0cl  20725  primefld1cl  20726  abvn0b  20755  suborng  20795  islss4  20899  lss1d  20900  lssintcl  20901  lspsolvlem  21083  lbsextlem1  21099  dflidl2rng  21159  lidlsubg  21164  rhmpreimaidl  21218  zringlpirlem1  21403  ocvlss  21613  lmiclbs  21778  lmisfree  21783  psrbas  21874  mplsubglem  21939  mplind  22008  mhpsubg  22071  mat1ric  22405  dmatsgrp  22417  scmatsgrp  22437  scmatsgrp1  22440  scmatlss  22443  scmatric  22455  cpmatsubgpmat  22638  matcpmric  22677  pmmpric  22741  clscld  22965  2ndcdisj  23374  dfac14lem  23535  opnfbas  23760  isfil2  23774  filn0  23780  filssufilg  23829  rnelfmlem  23870  flimfnfcls  23946  ptcmplem2  23971  clssubg  24027  tgpconncomp  24031  tsmsfbas  24046  ustfilxp  24131  ustne0  24132  xbln0  24332  bln0  24333  metustfbas  24475  metustbl  24484  nrgdomn  24589  icccmplem2  24742  icccmplem3  24743  reconnlem2  24746  phtpcer  24924  reparpht  24928  phtpcco2  24929  pcohtpy  24950  pcorevlem  24956  isclmp  25027  iscmet3lem2  25222  bcthlem4  25257  minveclem3b  25358  ivthlem2  25383  ivthlem3  25384  evthicc  25390  ovollb2  25420  ovolunlem1a  25427  ovolunlem1  25428  ovoliunlem1  25433  ovoliun2  25437  ioombl1lem4  25492  uniioombllem1  25512  uniioombllem2  25514  uniioombllem6  25519  mbfsup  25595  mbfinf  25596  mbflimsup  25597  itg2monolem1  25681  itg2mono  25684  ulm0  26330  pilem2  26392  pilem3  26393  ftalem3  27015  ftalem4  27016  ftalem5  27017  dchrabs  27201  pntlem3  27550  nocvxminlem  27720  tglnne0  28621  axlowdim1  28941  nvo00  30745  nmorepnf  30752  minvecolem1  30858  wrdpmtrlast  33071  cycpmco2lem5  33108  elrgspnlem1  33218  primefldchr  33276  fldgensdrg  33289  nsgqusf1olem1  33387  intlidl  33394  idlinsubrg  33405  rhmimaidl  33406  ssdifidl  33431  ssdifidlprm  33432  ssmxidl  33448  pidufd  33517  1arithufdlem1  33518  ply1dg1rtn0  33553  ply1degltlss  33566  exsslsb  33632  constrsdrg  33811  ordtconnlem1  33960  rrhre  34057  sigagenval  34176  oddpwdc  34390  bnj1177  35041  bnj1523  35106  rankfilimbi  35135  erdszelem8  35265  txsconnlem  35307  cvxsconn  35310  cvmsss2  35341  cvmliftmolem2  35349  cvmlift2lem12  35381  cvmliftpht  35385  finminlem  36385  onint1  36516  weiunlem2  36530  weiunfr  36534  finxpreclem4  37461  heicant  37718  itg2addnc  37737  ftc1anclem7  37762  ftc1anc  37764  prdsbnd2  37858  lkrlss  39217  pclvalN  40012  dian0  41161  docaclN  41246  dicn0  41314  dihglblem5  41420  dihglb2  41464  doch2val2  41486  dochocss  41488  lclkr  41655  lclkrs  41661  lcfr  41707  aks6d1c6lem3  42288  unitscyglem2  42312  qsalrel  42361  nacsfix  42832  mzpcln0  42848  rencldnfilem  42940  fnwe2lem2  43171  kelac1  43183  harn0  43222  hbtlem2  43244  naddwordnexlem4  43521  omltoe  43527  gneispa  44250  imo72b2lem0  44285  scottrankd  44368  relpfrlem  45073  ubelsupr  45144  suprnmpt  45298  disjinfi  45316  suprubrnmpt2  45376  suprubrnmpt  45377  ssfiunibd  45437  allbutfi  45518  allbutfiinf  45545  uzn0d  45550  uzublem  45555  climinf  45733  limclr  45780  climinf2lem  45831  limsupubuzlem  45837  liminflelimsupuz  45910  cnrefiisplem  45954  ioodvbdlimc1lem1  46056  ioodvbdlimc1  46058  ioodvbdlimc2  46060  stoweidlem36  46161  fourierdlem20  46252  fourierdlem25  46257  fourierdlem31  46263  fourierdlem37  46269  fourierdlem46  46277  fourierdlem52  46283  fourierdlem54  46285  fouriercn  46357  elaa2lem  46358  salgenval  46446  salgenn0  46456  sge0isum  46552  sge0reuzb  46573  ovnlerp  46687  ovnf  46688  hsphoidmvle2  46710  hsphoidmvle  46711  hoiprodp1  46713  hoidmv1lelem1  46716  hoidmv1lelem3  46718  hoidmv1le  46719  hoidifhspdmvle  46745  hspmbllem1  46751  hspmbllem3  46753  ovnovollem2  46782  smflimlem1  46896  smfsuplem1  46936  smfsuplem3  46938  smflimsuplem5  46949  smflimsuplem7  46951  preimafvn0  47507  lincolss  48562  fvconstr2  48991  catprs  49139  discsubc  49192  iinfconstbas  49194  eloppf  49261  eloppf2  49262  oppcup3  49337  oppcthinendcALT  49569  termcterm3  49643  termcciso  49644  idfudiag1bas  49652  idfudiag1  49653