Theorem ne0d 4288

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ≠ wne 2956  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-dif 3902  df-nul 4280

This theorem is used by:  snnzg  4735  prnzg  4739  eqsnd  4791  exss  5431  isofrlem  7340  peano3  7891  fvmpocurryd  8272  onnseq  8336  oeoalem  8589  oeoelem  8591  oeeui  8595  nnawordex  8630  omxpenlem  9081  frfi  9260  supgtoreq  9447  infltoreq  9480  cantnfp1lem2  9664  cantnfp1lem3  9665  oemapvali  9669  cantnflem1a  9670  cantnflem1d  9673  cantnflem1  9674  epfrs  9716  rankfilimbi  9883  scottrankd  9930  dfac9  10196  axdc3lem4  10512  intwun  10801  r1limwun  10802  gruina  10884  grur1a  10885  mulclpi  10959  indpi  10973  supsrlem  11177  axpre-sup  11235  supfirege  12285  uzn0  12963  suprzub  13047  fzn0  13651  flval3  13935  icopnfsup  13985  hashelne0d  14492  dfrtrcl2  15195  01sqrexlem3  15391  isercolllem2  15813  isercolllem3  15814  climsup  15817  mertenslem2  16034  gcdcllem1  16649  pclem  16996  prmreclem1  17074  4sqlem13  17115  vdwmc2  17137  vdwlem6  17144  vdwnnlem3  17155  prmgaplem3  17211  prmgaplem4  17212  mrcflem  17760  mrcval  17764  iscatd2  17835  chnub  18776  mndbn0  18920  grpbn0  19157  issubgrpd2  19333  issubg4  19336  subgint  19341  nmzsubg  19355  cycsubgcl  19401  ghmpreima  19432  gastacl  19503  sylow1lem5  19796  pgpssslw  19808  sylow2alem2  19812  sylow2blem3  19816  fislw  19819  sylow3lem4  19824  torsubg  20048  oddvdssubg  20049  iscygd  20081  iscygodd  20082  dprdsubg  20220  ablfac1eu  20269  simpgnideld  20295  submomnd  20326  01eq0ring  20761  cntzsubrng  20799  cntzsubr  20838  imadrhmcl  21034  primefld  21042  primefld0cl  21043  primefld1cl  21044  abvn0b  21073  suborng  21113  islss4  21217  lss1d  21218  lssintcl  21219  lspsolvlem  21400  lbsextlem1  21416  dflidl2rng  21477  lidlsubg  21482  lidlunin0  21495  rhmpreimaidl  21551  ssdifidl  21621  ssdifidlprm  21622  zringlpirlem1  21748  ocvlss  21958  lmiclbs  22123  lmisfree  22128  psrbas  22222  mplsubglem  22286  mplind  22359  mhpsubg  22454  mat1ric  22782  dmatsgrp  22794  scmatsgrp  22814  scmatsgrp1  22817  scmatlss  22820  scmatric  22832  cpmatsubgpmat  23018  matcpmric  23057  pmmpric  23121  clscld  23345  2ndcdisj  23755  dfac14lem  23916  opnfbas  24141  isfil2  24155  filn0  24161  filssufilg  24210  rnelfmlem  24251  flimfnfcls  24327  ptcmplem2  24352  clssubg  24408  tgpconncomp  24412  tsmsfbas  24427  ustfilxp  24512  ustne0  24513  xbln0  24713  bln0  24714  metustfbas  24856  metustbl  24865  nrgdomn  24970  icccmplem2  25123  icccmplem3  25124  reconnlem2  25127  phtpcer  25296  reparpht  25299  phtpcco2  25300  pcohtpy  25321  pcorevlem  25327  isclmp  25398  iscmet3lem2  25593  bcthlem4  25628  minveclem3b  25729  ivthlem2  25753  ivthlem3  25754  evthicc  25760  ovollb2  25790  ovolunlem1a  25797  ovolunlem1  25798  ovoliunlem1  25803  ovoliun2  25807  ioombl1lem4  25862  uniioombllem1  25882  uniioombllem2  25884  uniioombllem6  25889  mbfsup  25965  mbfinf  25966  mbflimsup  25967  itg2monolem1  26051  itg2mono  26054  ulm0  26700  pilem2  26761  pilem3  26762  ftalem3  27384  ftalem4  27385  ftalem5  27386  dchrabs  27569  pntlem3  27918  nocvxminlem  28122  bdayfinbndlem1  28835  tglnne0  29091  tglnpt4  29105  lnoppinn0  29213  angmgmaddeu2  29362  angmgmaddeu3  29363  angmgmaddov2lem  29369  angmgmaddcpbl  29372  angmgmaddrid  29375  prlngmolem1  29412  prlngmolem2  29413  prlngmo2  29416  prlngpln4  29418  prlngsymquadlem  29423  quadcgrprlng  29426  axlowdim1  29519  nvo00  31345  nmorepnf  31352  minvecolem1  31458  wrdpmtrlast  33636  cycpmco2lem5  33673  elrgspnlem1  33785  primefldchr  33845  fldgensdrg  33858  nsgqusf1olem1  33946  intlidl  33952  idlinsubrg  33963  rhmimaidl  33964  ssmxidl  33981  dflringlem2  34009  pidufd  34057  1arithufdlem1  34058  ply1dg1rtn0  34095  ply1degltlss  34110  exsslsb  34211  constrsdrg  34389  ordtconnlem1  34538  rrhre  34635  sigagenval  34755  oddpwdc  34969  bnj1177  35619  bnj1523  35684  erdszelem8  35932  txsconnlem  35974  cvxsconn  35977  cvmsss2  36008  cvmliftmolem2  36016  cvmlift2lem12  36048  cvmliftpht  36052  finminlem  37076  onint1  37207  weiunlem  37221  weiunfr  37225  finxpreclem4  38285  heicant  38541  itg2addnc  38560  ftc1anclem7  38585  ftc1anc  38587  prdsbnd2  38697  lkrlss  40120  pclvalN  40915  dian0  42064  docaclN  42149  dicn0  42217  dihglblem5  42323  dihglb2  42367  doch2val2  42389  dochocss  42391  lclkr  42558  lclkrs  42564  lcfr  42610  aks6d1c6lem3  43190  unitscyglem2  43214  qsalrel  43260  nacsfix  43676  mzpcln0  43692  rencldnfilem  43780  fnwe2lem2  44011  kelac1  44023  harn0  44062  hbtlem2  44084  naddwordnexlem4  44361  omltoe  44366  gneispa  45089  imo72b2lem0  45124  relpfrlem  45895  ubelsupr  45980  suprnmpt  46132  disjinfi  46150  suprubrnmpt2  46207  suprubrnmpt  46208  ssfiunibd  46268  allbutfi  46348  allbutfiinf  46374  uzn0d  46379  uzublem  46384  climinf  46562  limclr  46609  climinf2lem  46660  limsupubuzlem  46666  liminflelimsupuz  46739  cnrefiisplem  46783  ioodvbdlimc1lem1  46885  ioodvbdlimc1  46887  ioodvbdlimc2  46889  stoweidlem36  46990  fourierdlem20  47081  fourierdlem25  47086  fourierdlem31  47092  fourierdlem37  47098  fourierdlem46  47106  fourierdlem48  47108  fourierdlem49  47109  fourierdlem52  47112  fourierdlem54  47114  fouriercn  47186  elaa2lem  47187  salgenval  47275  salgenn0  47285  sge0isum  47381  sge0reuzb  47402  ovnlerp  47516  ovnf  47517  hsphoidmvle2  47539  hsphoidmvle  47540  hoiprodp1  47542  hoidmv1lelem1  47545  hoidmv1lelem3  47547  hoidmv1le  47548  hoidifhspdmvle  47574  hspmbllem1  47580  hspmbllem3  47582  ovnovollem2  47611  smflimlem1  47725  smfsuplem1  47765  smfsuplem3  47767  smflimsuplem5  47778  smflimsuplem7  47780  preimafvn0  48406  lincolss  49490  elovconstbrd  49918  catprs  50063  discsubc  50116  iinfconstbas  50118  eloppf  50185  eloppf2  50186  oppcup3  50261  oppcthinendcALT  50493  termcterm3  50567  termcciso  50568  idfudiag1bas  50576  idfudiag1  50577