Theorem ne0d 4335

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

Syntax hints:   → wi 4   ∈ wcel 2107   ≠ wne 2941  ∅c0 4322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-dif 3951  df-nul 4323

This theorem is referenced by:  snnzg  4778  prnzg  4782  exss  5463  isofrlem  7334  fvmpocurryd  8253  onnseq  8341  oeoalem  8593  oeoelem  8595  oeeui  8599  nnawordex  8634  omxpenlem  9070  frfi  9285  supgtoreq  9462  infltoreq  9494  cantnfp1lem2  9671  cantnfp1lem3  9672  oemapvali  9676  cantnflem1a  9677  cantnflem1d  9680  cantnflem1  9681  epfrs  9723  dfac9  10128  axdc3lem4  10445  intwun  10727  r1limwun  10728  gruina  10810  grur1a  10811  mulclpi  10885  indpi  10899  supsrlem  11103  axpre-sup  11161  supfirege  12198  uzn0  12836  suprzub  12920  fzn0  13512  flval3  13777  icopnfsup  13827  hashelne0d  14325  dfrtrcl2  15006  01sqrexlem3  15188  isercolllem2  15609  isercolllem3  15610  climsup  15613  mertenslem2  15828  gcdcllem1  16437  pclem  16768  prmreclem1  16846  4sqlem13  16887  vdwmc2  16909  vdwlem6  16916  vdwnnlem3  16927  prmgaplem3  16983  prmgaplem4  16984  mrcflem  17547  mrcval  17551  iscatd2  17622  mndbn0  18638  grpbn0  18848  issubgrpd2  19017  issubg4  19020  subgint  19025  nmzsubg  19040  cycsubgcl  19078  ghmpreima  19109  gastacl  19168  sylow1lem5  19465  pgpssslw  19477  sylow2alem2  19481  sylow2blem3  19485  fislw  19488  sylow3lem4  19493  torsubg  19717  oddvdssubg  19718  iscygd  19750  iscygodd  19751  dprdsubg  19889  ablfac1eu  19938  simpgnideld  19964  01eq0ring  20298  cntzsubr  20391  imadrhmcl  20406  primefld  20414  primefld0cl  20415  primefld1cl  20416  islss4  20566  lss1d  20567  lssintcl  20568  lspsolvlem  20748  lbsextlem1  20764  lidlsubg  20831  dflidl2lem  20835  abvn0b  20913  zringlpirlem1  21024  ocvlss  21217  lmiclbs  21384  lmisfree  21389  psrbas  21489  mplsubglem  21550  mplind  21623  mhpsubg  21688  mat1ric  21981  dmatsgrp  21993  scmatsgrp  22013  scmatsgrp1  22016  scmatlss  22019  scmatric  22031  cpmatsubgpmat  22214  matcpmric  22253  pmmpric  22317  clscld  22543  2ndcdisj  22952  dfac14lem  23113  opnfbas  23338  isfil2  23352  filn0  23358  filssufilg  23407  rnelfmlem  23448  flimfnfcls  23524  ptcmplem2  23549  clssubg  23605  tgpconncomp  23609  tsmsfbas  23624  ustfilxp  23709  ustne0  23710  xbln0  23912  bln0  23913  metustfbas  24058  metustbl  24067  nrgdomn  24180  icccmplem2  24331  icccmplem3  24332  reconnlem2  24335  phtpcer  24503  reparpht  24506  phtpcco2  24507  pcohtpy  24528  pcorevlem  24534  isclmp  24605  iscmet3lem2  24801  bcthlem4  24836  minveclem3b  24937  ivthlem2  24961  ivthlem3  24962  evthicc  24968  ovollb2  24998  ovolunlem1a  25005  ovolunlem1  25006  ovoliunlem1  25011  ovoliun2  25015  ioombl1lem4  25070  uniioombllem1  25090  uniioombllem2  25092  uniioombllem6  25097  mbfsup  25173  mbfinf  25174  mbflimsup  25175  itg2monolem1  25260  itg2mono  25263  ulm0  25895  pilem2  25956  pilem3  25957  ftalem3  26569  ftalem4  26570  ftalem5  26571  dchrabs  26753  pntlem3  27102  nocvxminlem  27269  tglnne0  27881  axlowdim1  28207  nvo00  30002  nmorepnf  30009  minvecolem1  30115  submomnd  32216  cycpmco2lem5  32277  primefldchr  32388  fldgensdrg  32393  suborng  32422  nsgqusf1olem1  32513  intlidl  32525  rhmpreimaidl  32526  idlinsubrg  32538  rhmimaidl  32539  ssmxidl  32579  ply1degltlss  32656  ordtconnlem1  32893  rrhre  32990  sigagenval  33127  oddpwdc  33342  bnj1177  34006  bnj1523  34071  erdszelem8  34178  txsconnlem  34220  cvxsconn  34223  cvmsss2  34254  cvmliftmolem2  34262  cvmlift2lem12  34294  cvmliftpht  34298  finminlem  35192  onint1  35323  finxpreclem4  36264  heicant  36512  itg2addnc  36531  ftc1anclem7  36556  ftc1anc  36558  prdsbnd2  36652  lkrlss  37954  pclvalN  38750  dian0  39899  docaclN  39984  dicn0  40052  dihglblem5  40158  dihglb2  40202  doch2val2  40224  dochocss  40226  lclkr  40393  lclkrs  40399  lcfr  40445  qsalrel  41060  nacsfix  41436  mzpcln0  41452  rencldnfilem  41544  fnwe2lem2  41779  kelac1  41791  harn0  41830  hbtlem2  41852  naddwordnexlem4  42138  omltoe  42144  gneispa  42867  scottrankd  42993  ubelsupr  43690  suprnmpt  43856  disjinfi  43877  suprubrnmpt2  43943  suprubrnmpt  43944  ssfiunibd  44006  allbutfi  44090  allbutfiinf  44117  uzn0d  44122  uzublem  44127  climinf  44309  limclr  44358  climinf2lem  44409  limsupubuzlem  44415  liminflelimsupuz  44488  cnrefiisplem  44532  ioodvbdlimc1lem1  44634  ioodvbdlimc1  44636  ioodvbdlimc2  44638  stoweidlem36  44739  fourierdlem20  44830  fourierdlem25  44835  fourierdlem31  44841  fourierdlem37  44847  fourierdlem46  44855  fourierdlem52  44861  fourierdlem54  44863  fouriercn  44935  elaa2lem  44936  salgenval  45024  salgenn0  45034  sge0isum  45130  sge0reuzb  45151  ovnlerp  45265  ovnf  45266  hsphoidmvle2  45288  hsphoidmvle  45289  hoiprodp1  45291  hoidmv1lelem1  45294  hoidmv1lelem3  45296  hoidmv1le  45297  hoidifhspdmvle  45323  hspmbllem1  45329  hspmbllem3  45331  ovnovollem2  45360  smflimlem1  45474  smfsuplem1  45514  smfsuplem3  45516  smflimsuplem5  45527  smflimsuplem7  45529  preimafvn0  46035  cntzsubrng  46731  lincolss  47069  fvconstr2  47478  catprs  47585