Theorem ne0d 4277

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

Syntax hints:   → wi 4   ∈ wcel 2119   ≠ wne 2935  ∅c0 4268

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 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-dif 3893  df-nul 4269

This theorem is referenced by:  snnzg  4713  prnzg  4717  eqsnd  4768  exss  5409  isofrlem  7291  fvmpocurryd  8218  onnseq  8281  oeoalem  8529  oeoelem  8531  oeeui  8535  nnawordex  8570  omxpenlem  9013  frfi  9192  supgtoreq  9381  infltoreq  9414  cantnfp1lem2  9598  cantnfp1lem3  9599  oemapvali  9603  cantnflem1a  9604  cantnflem1d  9607  cantnflem1  9608  epfrs  9650  dfac9  10057  axdc3lem4  10373  intwun  10656  r1limwun  10657  gruina  10739  grur1a  10740  mulclpi  10814  indpi  10828  supsrlem  11032  axpre-sup  11090  supfirege  12141  uzn0  12803  suprzub  12887  fzn0  13490  flval3  13772  icopnfsup  13822  hashelne0d  14328  dfrtrcl2  15022  01sqrexlem3  15204  isercolllem2  15626  isercolllem3  15627  climsup  15630  mertenslem2  15848  gcdcllem1  16466  pclem  16807  prmreclem1  16885  4sqlem13  16926  vdwmc2  16948  vdwlem6  16955  vdwnnlem3  16966  prmgaplem3  17022  prmgaplem4  17023  mrcflem  17570  mrcval  17574  iscatd2  17645  chnub  18586  mndbn0  18716  grpbn0  18940  issubgrpd2  19116  issubg4  19119  subgint  19124  nmzsubg  19138  cycsubgcl  19179  ghmpreima  19211  gastacl  19282  sylow1lem5  19575  pgpssslw  19587  sylow2alem2  19591  sylow2blem3  19595  fislw  19598  sylow3lem4  19603  torsubg  19827  oddvdssubg  19828  iscygd  19860  iscygodd  19861  dprdsubg  19999  ablfac1eu  20048  simpgnideld  20074  submomnd  20105  01eq0ring  20509  cntzsubrng  20546  cntzsubr  20585  imadrhmcl  20776  primefld  20784  primefld0cl  20785  primefld1cl  20786  abvn0b  20815  suborng  20855  islss4  20959  lss1d  20960  lssintcl  20961  lspsolvlem  21142  lbsextlem1  21158  dflidl2rng  21218  lidlsubg  21223  rhmpreimaidl  21277  zringlpirlem1  21444  ocvlss  21654  lmiclbs  21819  lmisfree  21824  psrbas  21916  mplsubglem  21980  mplind  22053  mhpsubg  22148  mat1ric  22477  dmatsgrp  22489  scmatsgrp  22509  scmatsgrp1  22512  scmatlss  22515  scmatric  22527  cpmatsubgpmat  22710  matcpmric  22749  pmmpric  22813  clscld  23037  2ndcdisj  23446  dfac14lem  23607  opnfbas  23832  isfil2  23846  filn0  23852  filssufilg  23901  rnelfmlem  23942  flimfnfcls  24018  ptcmplem2  24043  clssubg  24099  tgpconncomp  24103  tsmsfbas  24118  ustfilxp  24203  ustne0  24204  xbln0  24404  bln0  24405  metustfbas  24547  metustbl  24556  nrgdomn  24661  icccmplem2  24814  icccmplem3  24815  reconnlem2  24818  phtpcer  24987  reparpht  24990  phtpcco2  24991  pcohtpy  25012  pcorevlem  25018  isclmp  25089  iscmet3lem2  25284  bcthlem4  25319  minveclem3b  25420  ivthlem2  25444  ivthlem3  25445  evthicc  25451  ovollb2  25481  ovolunlem1a  25488  ovolunlem1  25489  ovoliunlem1  25494  ovoliun2  25498  ioombl1lem4  25553  uniioombllem1  25573  uniioombllem2  25575  uniioombllem6  25580  mbfsup  25656  mbfinf  25657  mbflimsup  25658  itg2monolem1  25742  itg2mono  25745  ulm0  26381  pilem2  26442  pilem3  26443  ftalem3  27063  ftalem4  27064  ftalem5  27065  dchrabs  27248  pntlem3  27597  nocvxminlem  27771  bdayfinbndlem1  28484  tglnne0  28733  axlowdim1  29053  nvo00  30857  nmorepnf  30864  minvecolem1  30970  wrdpmtrlast  33181  cycpmco2lem5  33218  elrgspnlem1  33330  primefldchr  33392  fldgensdrg  33405  nsgqusf1olem1  33503  intlidl  33510  idlinsubrg  33521  rhmimaidl  33522  ssdifidl  33547  ssdifidlprm  33548  ssmxidl  33564  pidufd  33633  1arithufdlem1  33634  ply1dg1rtn0  33671  ply1degltlss  33686  exsslsb  33788  constrsdrg  33966  ordtconnlem1  34115  rrhre  34212  sigagenval  34331  oddpwdc  34545  bnj1177  35195  bnj1523  35260  rankfilimbi  35289  erdszelem8  35433  txsconnlem  35475  cvxsconn  35478  cvmsss2  35509  cvmliftmolem2  35517  cvmlift2lem12  35549  cvmliftpht  35553  finminlem  36553  onint1  36684  weiunlem  36698  weiunfr  36702  finxpreclem4  37763  heicant  38029  itg2addnc  38048  ftc1anclem7  38073  ftc1anc  38075  prdsbnd2  38169  lkrlss  39594  pclvalN  40389  dian0  41538  docaclN  41623  dicn0  41691  dihglblem5  41797  dihglb2  41841  doch2val2  41863  dochocss  41865  lclkr  42032  lclkrs  42038  lcfr  42084  aks6d1c6lem3  42664  unitscyglem2  42688  qsalrel  42732  nacsfix  43168  mzpcln0  43184  rencldnfilem  43272  fnwe2lem2  43503  kelac1  43515  harn0  43554  hbtlem2  43576  naddwordnexlem4  43853  omltoe  43858  gneispa  44581  imo72b2lem0  44616  scottrankd  44699  relpfrlem  45404  ubelsupr  45475  suprnmpt  45628  disjinfi  45646  suprubrnmpt2  45703  suprubrnmpt  45704  ssfiunibd  45764  allbutfi  45844  allbutfiinf  45870  uzn0d  45875  uzublem  45880  climinf  46058  limclr  46105  climinf2lem  46156  limsupubuzlem  46162  liminflelimsupuz  46235  cnrefiisplem  46279  ioodvbdlimc1lem1  46381  ioodvbdlimc1  46383  ioodvbdlimc2  46385  stoweidlem36  46486  fourierdlem20  46577  fourierdlem25  46582  fourierdlem31  46588  fourierdlem37  46594  fourierdlem46  46602  fourierdlem52  46608  fourierdlem54  46610  fouriercn  46682  elaa2lem  46683  salgenval  46771  salgenn0  46781  sge0isum  46877  sge0reuzb  46898  ovnlerp  47012  ovnf  47013  hsphoidmvle2  47035  hsphoidmvle  47036  hoiprodp1  47038  hoidmv1lelem1  47041  hoidmv1lelem3  47043  hoidmv1le  47044  hoidifhspdmvle  47070  hspmbllem1  47076  hspmbllem3  47078  ovnovollem2  47107  smflimlem1  47221  smfsuplem1  47261  smfsuplem3  47263  smflimsuplem5  47274  smflimsuplem7  47276  preimafvn0  47862  lincolss  48932  fvconstr2  49361  catprs  49508  discsubc  49561  iinfconstbas  49563  eloppf  49630  eloppf2  49631  oppcup3  49706  oppcthinendcALT  49938  termcterm3  50012  termcciso  50013  idfudiag1bas  50021  idfudiag1  50022