Theorem ne0d 4297

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

Syntax hints:   → wi 4   ∈ wcel 2145   ≠ wne 2960  ∅c0 4288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-dif 3910  df-nul 4289

This theorem is referenced by:  snnzg  4736  prnzg  4740  eqsnd  4791  exss  5435  isofrlem  7328  peano3  7875  fvmpocurryd  8255  onnseq  8319  oeoalem  8570  oeoelem  8572  oeeui  8576  nnawordex  8611  omxpenlem  9054  frfi  9233  supgtoreq  9419  infltoreq  9452  cantnfp1lem2  9636  cantnfp1lem3  9637  oemapvali  9641  cantnflem1a  9642  cantnflem1d  9645  cantnflem1  9646  epfrs  9688  scottrankd  9862  dfac9  10108  axdc3lem4  10425  intwun  10708  r1limwun  10709  gruina  10791  grur1a  10792  mulclpi  10866  indpi  10880  supsrlem  11084  axpre-sup  11142  supfirege  12193  uzn0  12870  suprzub  12954  fzn0  13557  flval3  13839  icopnfsup  13889  hashelne0d  14395  dfrtrcl2  15089  01sqrexlem3  15285  isercolllem2  15707  isercolllem3  15708  climsup  15711  mertenslem2  15929  gcdcllem1  16547  pclem  16888  prmreclem1  16966  4sqlem13  17007  vdwmc2  17029  vdwlem6  17036  vdwnnlem3  17047  prmgaplem3  17103  prmgaplem4  17104  mrcflem  17652  mrcval  17656  iscatd2  17727  chnub  18668  mndbn0  18798  grpbn0  19023  issubgrpd2  19200  issubg4  19203  subgint  19208  nmzsubg  19222  cycsubgcl  19268  ghmpreima  19299  gastacl  19370  sylow1lem5  19663  pgpssslw  19675  sylow2alem2  19679  sylow2blem3  19683  fislw  19686  sylow3lem4  19691  torsubg  19915  oddvdssubg  19916  iscygd  19948  iscygodd  19949  dprdsubg  20087  ablfac1eu  20136  simpgnideld  20162  submomnd  20193  01eq0ring  20605  cntzsubrng  20643  cntzsubr  20682  imadrhmcl  20869  primefld  20877  primefld0cl  20878  primefld1cl  20879  abvn0b  20908  suborng  20948  islss4  21052  lss1d  21053  lssintcl  21054  lspsolvlem  21235  lbsextlem1  21251  dflidl2rng  21312  lidlsubg  21317  lidlunin0  21330  rhmpreimaidl  21378  ssdifidl  21445  ssdifidlprm  21446  zringlpirlem1  21572  ocvlss  21782  lmiclbs  21947  lmisfree  21952  psrbas  22044  mplsubglem  22108  mplind  22181  mhpsubg  22276  mat1ric  22605  dmatsgrp  22617  scmatsgrp  22637  scmatsgrp1  22640  scmatlss  22643  scmatric  22655  cpmatsubgpmat  22838  matcpmric  22877  pmmpric  22941  clscld  23165  2ndcdisj  23574  dfac14lem  23735  opnfbas  23960  isfil2  23974  filn0  23980  filssufilg  24029  rnelfmlem  24070  flimfnfcls  24146  ptcmplem2  24171  clssubg  24227  tgpconncomp  24231  tsmsfbas  24246  ustfilxp  24331  ustne0  24332  xbln0  24532  bln0  24533  metustfbas  24675  metustbl  24684  nrgdomn  24789  icccmplem2  24942  icccmplem3  24943  reconnlem2  24946  phtpcer  25115  reparpht  25118  phtpcco2  25119  pcohtpy  25140  pcorevlem  25146  isclmp  25217  iscmet3lem2  25412  bcthlem4  25447  minveclem3b  25548  ivthlem2  25572  ivthlem3  25573  evthicc  25579  ovollb2  25609  ovolunlem1a  25616  ovolunlem1  25617  ovoliunlem1  25622  ovoliun2  25626  ioombl1lem4  25681  uniioombllem1  25701  uniioombllem2  25703  uniioombllem6  25708  mbfsup  25784  mbfinf  25785  mbflimsup  25786  itg2monolem1  25870  itg2mono  25873  ulm0  26512  pilem2  26573  pilem3  26574  ftalem3  27197  ftalem4  27198  ftalem5  27199  dchrabs  27382  pntlem3  27731  nocvxminlem  27905  bdayfinbndlem1  28618  tglnne0  28868  tglnpt4  28882  axlowdim1  29218  nvo00  31022  nmorepnf  31029  minvecolem1  31135  wrdpmtrlast  33326  cycpmco2lem5  33363  elrgspnlem1  33475  primefldchr  33537  fldgensdrg  33550  nsgqusf1olem1  33638  intlidl  33644  idlinsubrg  33655  rhmimaidl  33656  ssmxidl  33674  dflringlem2  33702  pidufd  33750  1arithufdlem1  33751  ply1dg1rtn0  33788  ply1degltlss  33803  exsslsb  33904  constrsdrg  34082  ordtconnlem1  34231  rrhre  34328  sigagenval  34447  oddpwdc  34661  bnj1177  35311  bnj1523  35376  rankfilimbi  35409  erdszelem8  35561  txsconnlem  35603  cvxsconn  35606  cvmsss2  35637  cvmliftmolem2  35645  cvmlift2lem12  35677  cvmliftpht  35681  finminlem  36691  onint1  36822  weiunlem  36836  weiunfr  36840  finxpreclem4  37900  heicant  38166  itg2addnc  38185  ftc1anclem7  38210  ftc1anc  38212  prdsbnd2  38306  lkrlss  39731  pclvalN  40526  dian0  41675  docaclN  41760  dicn0  41828  dihglblem5  41934  dihglb2  41978  doch2val2  42000  dochocss  42002  lclkr  42169  lclkrs  42175  lcfr  42221  aks6d1c6lem3  42801  unitscyglem2  42825  qsalrel  42869  nacsfix  43305  mzpcln0  43321  rencldnfilem  43409  fnwe2lem2  43640  kelac1  43652  harn0  43691  hbtlem2  43713  naddwordnexlem4  43990  omltoe  43995  gneispa  44718  imo72b2lem0  44753  relpfrlem  45527  ubelsupr  45598  suprnmpt  45750  disjinfi  45768  suprubrnmpt2  45825  suprubrnmpt  45826  ssfiunibd  45886  allbutfi  45966  allbutfiinf  45992  uzn0d  45997  uzublem  46002  climinf  46180  limclr  46227  climinf2lem  46278  limsupubuzlem  46284  liminflelimsupuz  46357  cnrefiisplem  46401  ioodvbdlimc1lem1  46503  ioodvbdlimc1  46505  ioodvbdlimc2  46507  stoweidlem36  46608  fourierdlem20  46699  fourierdlem25  46704  fourierdlem31  46710  fourierdlem37  46716  fourierdlem46  46724  fourierdlem48  46726  fourierdlem49  46727  fourierdlem52  46730  fourierdlem54  46732  fouriercn  46804  elaa2lem  46805  salgenval  46893  salgenn0  46903  sge0isum  46999  sge0reuzb  47020  ovnlerp  47134  ovnf  47135  hsphoidmvle2  47157  hsphoidmvle  47158  hoiprodp1  47160  hoidmv1lelem1  47163  hoidmv1lelem3  47165  hoidmv1le  47166  hoidifhspdmvle  47192  hspmbllem1  47198  hspmbllem3  47200  ovnovollem2  47229  smflimlem1  47343  smfsuplem1  47383  smfsuplem3  47385  smflimsuplem5  47396  smflimsuplem7  47398  preimafvn0  47984  lincolss  49065  fvconstr2  49493  catprs  49640  discsubc  49693  iinfconstbas  49695  eloppf  49762  eloppf2  49763  oppcup3  49838  oppcthinendcALT  50070  termcterm3  50144  termcciso  50145  idfudiag1bas  50153  idfudiag1  50154