Theorem ne0d 4287

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ≠ wne 2955  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-dif 4047  df-nul 4279

This theorem is used by:  snnzg  4731  prnzg  4735  eqsnd  4785  exss  5430  isofrlem  7348  peano3  7902  fnwe2lem3  8149  fvmpocurryd  8291  onnseq  8355  oeoalem  8608  oeoelem  8610  oeeui  8614  nnawordex  8649  omxpenlem  9100  frfi  9279  supgtoreq  9466  infltoreq  9499  cantnfp1lem2  9683  cantnfp1lem3  9684  oemapvali  9688  cantnflem1a  9689  cantnflem1d  9692  cantnflem1  9693  epfrs  9735  rankfilimbi  9905  scottrankd  9952  dfac9  10218  axdc3lem4  10534  intwun  10823  r1limwun  10824  gruina  10906  grur1a  10907  mulclpi  10981  indpi  10995  supsrlem  11199  axpre-sup  11257  supfirege  12307  uzn0  12985  suprzub  13069  fzn0  13674  flval3  13958  icopnfsup  14008  hashelne0d  14515  dfrtrcl2  15220  01sqrexlem3  15416  isercolllem2  15838  isercolllem3  15839  climsup  15842  mertenslem2  16059  gcdcllem1  16674  pclem  17021  prmreclem1  17099  4sqlem13  17140  vdwmc2  17162  vdwlem6  17169  vdwnnlem3  17180  prmgaplem3  17236  prmgaplem4  17237  mrcflem  17785  mrcval  17789  iscatd2  17860  chnub  18801  mndbn0  18945  grpbn0  19182  issubgrpd2  19358  issubg4  19361  subgint  19366  nmzsubg  19380  cycsubgcl  19426  ghmpreima  19457  gastacl  19528  sylow1lem5  19821  pgpssslw  19833  sylow2alem2  19837  sylow2blem3  19841  fislw  19844  sylow3lem4  19849  torsubg  20073  oddvdssubg  20074  iscygd  20106  iscygodd  20107  dprdsubg  20245  ablfac1eu  20294  simpgnideld  20320  submomnd  20351  01eq0ring  20786  cntzsubrng  20824  cntzsubr  20863  imadrhmcl  21059  primefld  21067  primefld0cl  21068  primefld1cl  21069  abvn0b  21098  suborng  21138  islss4  21242  lss1d  21243  lssintcl  21244  lspsolvlem  21425  lbsextlem1  21441  dflidl2rng  21502  lidlsubg  21507  lidlunin0  21520  rhmpreimaidl  21576  ssdifidl  21646  ssdifidlprm  21647  zringlpirlem1  21773  ocvlss  21983  lmiclbs  22148  lmisfree  22153  psrbas  22247  mplsubglem  22311  mplind  22384  mhpsubg  22479  mat1ric  22807  dmatsgrp  22819  scmatsgrp  22839  scmatsgrp1  22842  scmatlss  22845  scmatric  22857  cpmatsubgpmat  23043  matcpmric  23082  pmmpric  23146  clscld  23370  2ndcdisj  23780  dfac14lem  23941  opnfbas  24166  isfil2  24180  filn0  24186  filssufilg  24235  rnelfmlem  24276  flimfnfcls  24352  ptcmplem2  24377  clssubg  24433  tgpconncomp  24437  tsmsfbas  24452  ustfilxp  24537  ustne0  24538  xbln0  24738  bln0  24739  metustfbas  24881  metustbl  24890  nrgdomn  24995  icccmplem2  25148  icccmplem3  25149  reconnlem2  25152  phtpcer  25321  reparpht  25324  phtpcco2  25325  pcohtpy  25346  pcorevlem  25352  isclmp  25423  iscmet3lem2  25618  bcthlem4  25653  minveclem3b  25754  ivthlem2  25778  ivthlem3  25779  evthicc  25785  ovollb2  25815  ovolunlem1a  25822  ovolunlem1  25823  ovoliunlem1  25828  ovoliun2  25832  ioombl1lem4  25887  uniioombllem1  25907  uniioombllem2  25909  uniioombllem6  25914  mbfsup  25990  mbfinf  25991  mbflimsup  25992  itg2monolem1  26076  itg2mono  26079  ulm0  26723  pilem2  26784  pilem3  26785  ftalem3  27407  ftalem4  27408  ftalem5  27409  dchrabs  27592  pntlem3  27941  nocvxminlem  28145  bdayfinbndlem1  28858  tglnne0  29114  tglnpt4  29128  lnoppinn0  29236  angmgmaddeu2  29385  angmgmaddeu3  29386  angmgmaddov2lem  29392  angmgmaddcpbl  29395  angmgmaddrid  29398  prlngmolem1  29435  prlngmolem2  29436  prlngmo2  29439  prlngpln4  29441  prlngsymquadlem  29446  quadcgrprlng  29449  axlowdim1  29542  nvo00  31368  nmorepnf  31375  minvecolem1  31481  wrdpmtrlast  33700  cycpmco2lem5  33737  elrgspnlem1  33849  primefldchr  33909  fldgensdrg  33922  nsgqusf1olem1  34010  intlidl  34016  idlinsubrg  34027  rhmimaidl  34028  ssmxidl  34045  dflringlem2  34073  pidufd  34121  1arithufdlem1  34122  ply1dg1rtn0  34159  ply1degltlss  34174  exsslsb  34275  constrsdrg  34453  ordtconnlem1  34602  rrhre  34699  sigagenval  34819  oddpwdc  35032  bnj1177  35682  bnj1523  35747  erdszelem8  36049  txsconnlem  36091  cvxsconn  36094  cvmsss2  36125  cvmliftmolem2  36133  cvmlift2lem12  36165  cvmliftpht  36169  finminlem  37198  onint1  37329  weiunlem  37343  weiunfr  37347  finxpreclem4  38410  heicant  38666  itg2addnc  38685  ftc1anclem7  38710  ftc1anc  38712  prdsbnd2  38822  lkrlss  40245  pclvalN  41040  dian0  42189  docaclN  42274  dicn0  42342  dihglblem5  42448  dihglb2  42492  doch2val2  42514  dochocss  42516  lclkr  42683  lclkrs  42689  lcfr  42735  aks6d1c6lem3  43315  unitscyglem2  43339  qsalrel  43385  nacsfix  43816  mzpcln0  43832  rencldnfilem  43920  kelac1  44158  harn0  44197  hbtlem2  44219  naddwordnexlem4  44496  omltoe  44501  gneispa  45223  imo72b2lem0  45258  relpfrlem  46036  ubelsupr  46130  suprnmpt  46282  disjinfi  46300  suprubrnmpt2  46357  suprubrnmpt  46358  ssfiunibd  46418  allbutfi  46497  allbutfiinf  46523  uzn0d  46528  uzublem  46533  climinf  46711  limclr  46758  climinf2lem  46809  limsupubuzlem  46815  liminflelimsupuz  46888  cnrefiisplem  46932  ioodvbdlimc1lem1  47034  ioodvbdlimc1  47036  ioodvbdlimc2  47038  stoweidlem36  47139  fourierdlem20  47230  fourierdlem25  47235  fourierdlem31  47241  fourierdlem37  47247  fourierdlem46  47255  fourierdlem48  47257  fourierdlem49  47258  fourierdlem52  47261  fourierdlem54  47263  fouriercn  47335  elaa2lem  47336  salgenval  47424  salgenn0  47434  sge0isum  47530  sge0reuzb  47551  ovnlerp  47665  ovnf  47666  hsphoidmvle2  47688  hsphoidmvle  47689  hoiprodp1  47691  hoidmv1lelem1  47694  hoidmv1lelem3  47696  hoidmv1le  47697  hoidifhspdmvle  47723  hspmbllem1  47729  hspmbllem3  47731  ovnovollem2  47760  smflimlem1  47874  smfsuplem1  47914  smfsuplem3  47916  smflimsuplem5  47927  smflimsuplem7  47929  preimafvn0  48555  lincolss  49639  elovconstbrd  50068  catprs  50218  discsubc  50271  iinfconstbas  50273  eloppf  50342  eloppf2  50343  oppcup3  50418  oppcthinendcALT  50669  termcterm3  50743  termcciso  50744  idfudiag1bas  50752  idfudiag1  50753