Theorem ne0d 4282

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

Syntax hints:   → wi 4   ∈ wcel 2114   ≠ wne 2932  ∅c0 4273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-dif 3892  df-nul 4274

This theorem is referenced by:  snnzg  4718  prnzg  4722  eqsnd  4773  exss  5415  isofrlem  7295  fvmpocurryd  8221  onnseq  8284  oeoalem  8532  oeoelem  8534  oeeui  8538  nnawordex  8573  omxpenlem  9016  frfi  9195  supgtoreq  9384  infltoreq  9417  cantnfp1lem2  9600  cantnfp1lem3  9601  oemapvali  9605  cantnflem1a  9606  cantnflem1d  9609  cantnflem1  9610  epfrs  9652  dfac9  10059  axdc3lem4  10375  intwun  10658  r1limwun  10659  gruina  10741  grur1a  10742  mulclpi  10816  indpi  10830  supsrlem  11034  axpre-sup  11092  supfirege  12143  uzn0  12805  suprzub  12889  fzn0  13492  flval3  13774  icopnfsup  13824  hashelne0d  14330  dfrtrcl2  15024  01sqrexlem3  15206  isercolllem2  15628  isercolllem3  15629  climsup  15632  mertenslem2  15850  gcdcllem1  16468  pclem  16809  prmreclem1  16887  4sqlem13  16928  vdwmc2  16950  vdwlem6  16957  vdwnnlem3  16968  prmgaplem3  17024  prmgaplem4  17025  mrcflem  17572  mrcval  17576  iscatd2  17647  chnub  18588  mndbn0  18718  grpbn0  18942  issubgrpd2  19118  issubg4  19121  subgint  19126  nmzsubg  19140  cycsubgcl  19181  ghmpreima  19213  gastacl  19284  sylow1lem5  19577  pgpssslw  19589  sylow2alem2  19593  sylow2blem3  19597  fislw  19600  sylow3lem4  19605  torsubg  19829  oddvdssubg  19830  iscygd  19862  iscygodd  19863  dprdsubg  20001  ablfac1eu  20050  simpgnideld  20076  submomnd  20107  01eq0ring  20507  cntzsubrng  20544  cntzsubr  20583  imadrhmcl  20774  primefld  20782  primefld0cl  20783  primefld1cl  20784  abvn0b  20813  suborng  20853  islss4  20957  lss1d  20958  lssintcl  20959  lspsolvlem  21140  lbsextlem1  21156  dflidl2rng  21216  lidlsubg  21221  rhmpreimaidl  21275  zringlpirlem1  21442  ocvlss  21652  lmiclbs  21817  lmisfree  21822  psrbas  21913  mplsubglem  21977  mplind  22048  mhpsubg  22119  mat1ric  22452  dmatsgrp  22464  scmatsgrp  22484  scmatsgrp1  22487  scmatlss  22490  scmatric  22502  cpmatsubgpmat  22685  matcpmric  22724  pmmpric  22788  clscld  23012  2ndcdisj  23421  dfac14lem  23582  opnfbas  23807  isfil2  23821  filn0  23827  filssufilg  23876  rnelfmlem  23917  flimfnfcls  23993  ptcmplem2  24018  clssubg  24074  tgpconncomp  24078  tsmsfbas  24093  ustfilxp  24178  ustne0  24179  xbln0  24379  bln0  24380  metustfbas  24522  metustbl  24531  nrgdomn  24636  icccmplem2  24789  icccmplem3  24790  reconnlem2  24793  phtpcer  24962  reparpht  24965  phtpcco2  24966  pcohtpy  24987  pcorevlem  24993  isclmp  25064  iscmet3lem2  25259  bcthlem4  25294  minveclem3b  25395  ivthlem2  25419  ivthlem3  25420  evthicc  25426  ovollb2  25456  ovolunlem1a  25463  ovolunlem1  25464  ovoliunlem1  25469  ovoliun2  25473  ioombl1lem4  25528  uniioombllem1  25548  uniioombllem2  25550  uniioombllem6  25555  mbfsup  25631  mbfinf  25632  mbflimsup  25633  itg2monolem1  25717  itg2mono  25720  ulm0  26356  pilem2  26417  pilem3  26418  ftalem3  27038  ftalem4  27039  ftalem5  27040  dchrabs  27223  pntlem3  27572  nocvxminlem  27746  bdayfinbndlem1  28459  tglnne0  28708  axlowdim1  29028  nvo00  30832  nmorepnf  30839  minvecolem1  30945  wrdpmtrlast  33154  cycpmco2lem5  33191  elrgspnlem1  33303  primefldchr  33362  fldgensdrg  33375  nsgqusf1olem1  33473  intlidl  33480  idlinsubrg  33491  rhmimaidl  33492  ssdifidl  33517  ssdifidlprm  33518  ssmxidl  33534  pidufd  33603  1arithufdlem1  33604  ply1dg1rtn0  33641  ply1degltlss  33656  exsslsb  33741  constrsdrg  33919  ordtconnlem1  34068  rrhre  34165  sigagenval  34284  oddpwdc  34498  bnj1177  35148  bnj1523  35213  rankfilimbi  35244  erdszelem8  35380  txsconnlem  35422  cvxsconn  35425  cvmsss2  35456  cvmliftmolem2  35464  cvmlift2lem12  35496  cvmliftpht  35500  finminlem  36500  onint1  36631  weiunlem  36645  weiunfr  36649  finxpreclem4  37710  heicant  37976  itg2addnc  37995  ftc1anclem7  38020  ftc1anc  38022  prdsbnd2  38116  lkrlss  39541  pclvalN  40336  dian0  41485  docaclN  41570  dicn0  41638  dihglblem5  41744  dihglb2  41788  doch2val2  41810  dochocss  41812  lclkr  41979  lclkrs  41985  lcfr  42031  aks6d1c6lem3  42611  unitscyglem2  42635  qsalrel  42680  nacsfix  43144  mzpcln0  43160  rencldnfilem  43248  fnwe2lem2  43479  kelac1  43491  harn0  43530  hbtlem2  43552  naddwordnexlem4  43829  omltoe  43834  gneispa  44557  imo72b2lem0  44592  scottrankd  44675  relpfrlem  45380  ubelsupr  45451  suprnmpt  45604  disjinfi  45622  suprubrnmpt2  45681  suprubrnmpt  45682  ssfiunibd  45742  allbutfi  45822  allbutfiinf  45848  uzn0d  45853  uzublem  45858  climinf  46036  limclr  46083  climinf2lem  46134  limsupubuzlem  46140  liminflelimsupuz  46213  cnrefiisplem  46257  ioodvbdlimc1lem1  46359  ioodvbdlimc1  46361  ioodvbdlimc2  46363  stoweidlem36  46464  fourierdlem20  46555  fourierdlem25  46560  fourierdlem31  46566  fourierdlem37  46572  fourierdlem46  46580  fourierdlem52  46586  fourierdlem54  46588  fouriercn  46660  elaa2lem  46661  salgenval  46749  salgenn0  46759  sge0isum  46855  sge0reuzb  46876  ovnlerp  46990  ovnf  46991  hsphoidmvle2  47013  hsphoidmvle  47014  hoiprodp1  47016  hoidmv1lelem1  47019  hoidmv1lelem3  47021  hoidmv1le  47022  hoidifhspdmvle  47048  hspmbllem1  47054  hspmbllem3  47056  ovnovollem2  47085  smflimlem1  47199  smfsuplem1  47239  smfsuplem3  47241  smflimsuplem5  47252  smflimsuplem7  47254  preimafvn0  47840  lincolss  48910  fvconstr2  49339  catprs  49486  discsubc  49539  iinfconstbas  49541  eloppf  49608  eloppf2  49609  oppcup3  49684  oppcthinendcALT  49916  termcterm3  49990  termcciso  49991  idfudiag1bas  49999  idfudiag1  50000