Theorem ne0d 4234

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2935  ∅c0 4221

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-ne 2936  df-dif 3856  df-nul 4222

This theorem is referenced by:  snnzg  4675  prnzg  4679  exss  5331  isofrlem  7119  fvmpocurryd  7979  onnseq  8023  oeoalem  8266  oeoelem  8268  oeeui  8272  nnawordex  8307  omxpenlem  8680  frfi  8850  supgtoreq  9020  infltoreq  9052  cantnfp1lem2  9228  cantnfp1lem3  9229  oemapvali  9233  cantnflem1a  9234  cantnflem1d  9237  cantnflem1  9238  epfrs  9259  dfac9  9649  axdc3lem4  9966  intwun  10248  r1limwun  10249  gruina  10331  grur1a  10332  mulclpi  10406  indpi  10420  supsrlem  10624  axpre-sup  10682  supfirege  11718  uzn0  12354  suprzub  12434  fzn0  13025  flval3  13289  icopnfsup  13337  hashelne0d  13834  dfrtrcl2  14524  sqrlem3  14707  isercolllem2  15128  isercolllem3  15129  climsup  15132  mertenslem2  15346  gcdcllem1  15955  pclem  16288  prmreclem1  16365  4sqlem13  16406  vdwmc2  16428  vdwlem6  16435  vdwnnlem3  16446  prmgaplem3  16502  prmgaplem4  16503  mrcflem  16993  mrcval  16997  iscatd2  17068  mndbn0  18056  grpbn0  18263  issubgrpd2  18426  issubg4  18429  subgint  18434  nmzsubg  18448  cycsubgcl  18480  ghmpreima  18511  gastacl  18570  sylow1lem5  18858  pgpssslw  18870  sylow2alem2  18874  sylow2blem3  18878  fislw  18881  sylow3lem4  18886  torsubg  19106  oddvdssubg  19107  iscygd  19138  iscygodd  19139  dprdsubg  19278  ablfac1eu  19327  simpgnideld  19353  cntzsubr  19700  primefld  19716  primefld0cl  19717  primefld1cl  19718  islss4  19866  lss1d  19867  lssintcl  19868  lspsolvlem  20046  lbsextlem1  20062  lidlsubg  20120  abvn0b  20207  zringlpirlem1  20316  ocvlss  20501  lmiclbs  20666  lmisfree  20671  psrbas  20770  mplsubglem  20828  mplind  20895  mhpsubg  20960  mat1ric  21251  dmatsgrp  21263  scmatsgrp  21283  scmatsgrp1  21286  scmatlss  21289  scmatric  21301  cpmatsubgpmat  21484  matcpmric  21523  pmmpric  21587  clscld  21811  2ndcdisj  22220  dfac14lem  22381  opnfbas  22606  isfil2  22620  filn0  22626  filssufilg  22675  rnelfmlem  22716  flimfnfcls  22792  ptcmplem2  22817  clssubg  22873  tgpconncomp  22877  tsmsfbas  22892  ustfilxp  22977  ustne0  22978  xbln0  23180  bln0  23181  metustfbas  23323  metustbl  23332  nrgdomn  23437  icccmplem2  23588  icccmplem3  23589  reconnlem2  23592  phtpcer  23760  reparpht  23763  phtpcco2  23764  pcohtpy  23785  pcorevlem  23791  isclmp  23862  iscmet3lem2  24057  bcthlem4  24092  minveclem3b  24193  ivthlem2  24217  ivthlem3  24218  evthicc  24224  ovollb2  24254  ovolunlem1a  24261  ovolunlem1  24262  ovoliunlem1  24267  ovoliun2  24271  ioombl1lem4  24326  uniioombllem1  24346  uniioombllem2  24348  uniioombllem6  24353  mbfsup  24429  mbfinf  24430  mbflimsup  24431  itg2monolem1  24516  itg2mono  24519  ulm0  25151  pilem2  25212  pilem3  25213  ftalem3  25825  ftalem4  25826  ftalem5  25827  dchrabs  26009  pntlem3  26358  tglnne0  26599  axlowdim1  26918  nvo00  28709  nmorepnf  28716  minvecolem1  28822  submomnd  30926  cycpmco2lem5  30987  primefldchr  31083  suborng  31104  nsgqusf1olem1  31183  intlidl  31187  rhmpreimaidl  31188  idlinsubrg  31193  rhmimaidl  31194  ssmxidl  31227  ordtconnlem1  31459  rrhre  31554  sigagenval  31691  oddpwdc  31904  bnj1177  32570  bnj1523  32635  erdszelem8  32744  txsconnlem  32786  cvxsconn  32789  cvmsss2  32820  cvmliftmolem2  32828  cvmlift2lem12  32860  cvmliftpht  32864  nocvxminlem  33628  finminlem  34163  onint1  34294  finxpreclem4  35221  heicant  35468  itg2addnc  35487  ftc1anclem7  35512  ftc1anc  35514  prdsbnd2  35609  lkrlss  36765  pclvalN  37560  dian0  38709  docaclN  38794  dicn0  38862  dihglblem5  38968  dihglb2  39012  doch2val2  39034  dochocss  39036  lclkr  39203  lclkrs  39209  lcfr  39255  qsalrel  39838  nacsfix  40147  mzpcln0  40163  rencldnfilem  40255  fnwe2lem2  40489  kelac1  40501  harn0  40540  hbtlem2  40562  gneispa  41327  scottrankd  41449  ubelsupr  42142  suprnmpt  42289  disjinfi  42310  suprubrnmpt2  42376  suprubrnmpt  42377  ssfiunibd  42427  allbutfi  42512  allbutfiinf  42539  uzn0d  42544  uzublem  42549  climinf  42730  limclr  42779  climinf2lem  42830  limsupubuzlem  42836  liminflelimsupuz  42909  cnrefiisplem  42953  ioodvbdlimc1lem1  43055  ioodvbdlimc1  43057  ioodvbdlimc2  43059  stoweidlem36  43160  fourierdlem20  43251  fourierdlem25  43256  fourierdlem31  43262  fourierdlem37  43268  fourierdlem46  43276  fourierdlem52  43282  fourierdlem54  43284  fouriercn  43356  elaa2lem  43357  salgenval  43445  salgenn0  43453  sge0isum  43548  sge0reuzb  43569  ovnlerp  43683  ovnf  43684  hsphoidmvle2  43706  hsphoidmvle  43707  hoiprodp1  43709  hoidmv1lelem1  43712  hoidmv1lelem3  43714  hoidmv1le  43715  hoidifhspdmvle  43741  hspmbllem1  43747  hspmbllem3  43749  ovnovollem2  43778  smflimlem1  43886  smfsuplem1  43924  smfsuplem3  43926  smflimsuplem5  43937  smflimsuplem7  43939  preimafvn0  44414  lincolss  45357  fvconstr2  45756  catprs  45821