Theorem ne0d 4285

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

Syntax hints:   → wi 4   ∈ wcel 2132   ≠ wne 2947  ∅c0 4276

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1553  df-fal 1563  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-ne 2948  df-dif 3898  df-nul 4277

This theorem is referenced by:  snnzg  4723  prnzg  4727  eqsnd  4778  exss  5420  isofrlem  7309  peano3  7856  fvmpocurryd  8235  onnseq  8299  oeoalem  8550  oeoelem  8552  oeeui  8556  nnawordex  8591  omxpenlem  9035  frfi  9214  supgtoreq  9403  infltoreq  9436  cantnfp1lem2  9620  cantnfp1lem3  9621  oemapvali  9625  cantnflem1a  9626  cantnflem1d  9629  cantnflem1  9630  epfrs  9672  dfac9  10079  axdc3lem4  10396  intwun  10679  r1limwun  10680  gruina  10762  grur1a  10763  mulclpi  10837  indpi  10851  supsrlem  11055  axpre-sup  11113  supfirege  12165  uzn0  12842  suprzub  12926  fzn0  13529  flval3  13811  icopnfsup  13861  hashelne0d  14367  dfrtrcl2  15061  01sqrexlem3  15243  isercolllem2  15665  isercolllem3  15666  climsup  15669  mertenslem2  15887  gcdcllem1  16505  pclem  16846  prmreclem1  16924  4sqlem13  16965  vdwmc2  16987  vdwlem6  16994  vdwnnlem3  17005  prmgaplem3  17061  prmgaplem4  17062  mrcflem  17610  mrcval  17614  iscatd2  17685  chnub  18626  mndbn0  18756  grpbn0  18980  issubgrpd2  19156  issubg4  19159  subgint  19164  nmzsubg  19178  cycsubgcl  19219  ghmpreima  19250  gastacl  19321  sylow1lem5  19614  pgpssslw  19626  sylow2alem2  19630  sylow2blem3  19634  fislw  19637  sylow3lem4  19642  torsubg  19866  oddvdssubg  19867  iscygd  19899  iscygodd  19900  dprdsubg  20038  ablfac1eu  20087  simpgnideld  20113  submomnd  20144  01eq0ring  20548  cntzsubrng  20585  cntzsubr  20624  imadrhmcl  20815  primefld  20823  primefld0cl  20824  primefld1cl  20825  abvn0b  20854  suborng  20894  islss4  20998  lss1d  20999  lssintcl  21000  lspsolvlem  21181  lbsextlem1  21197  dflidl2rng  21257  lidlsubg  21262  rhmpreimaidl  21316  zringlpirlem1  21483  ocvlss  21693  lmiclbs  21858  lmisfree  21863  psrbas  21955  mplsubglem  22019  mplind  22092  mhpsubg  22187  mat1ric  22516  dmatsgrp  22528  scmatsgrp  22548  scmatsgrp1  22551  scmatlss  22554  scmatric  22566  cpmatsubgpmat  22749  matcpmric  22788  pmmpric  22852  clscld  23076  2ndcdisj  23485  dfac14lem  23646  opnfbas  23871  isfil2  23885  filn0  23891  filssufilg  23940  rnelfmlem  23981  flimfnfcls  24057  ptcmplem2  24082  clssubg  24138  tgpconncomp  24142  tsmsfbas  24157  ustfilxp  24242  ustne0  24243  xbln0  24443  bln0  24444  metustfbas  24586  metustbl  24595  nrgdomn  24700  icccmplem2  24853  icccmplem3  24854  reconnlem2  24857  phtpcer  25026  reparpht  25029  phtpcco2  25030  pcohtpy  25051  pcorevlem  25057  isclmp  25128  iscmet3lem2  25323  bcthlem4  25358  minveclem3b  25459  ivthlem2  25483  ivthlem3  25484  evthicc  25490  ovollb2  25520  ovolunlem1a  25527  ovolunlem1  25528  ovoliunlem1  25533  ovoliun2  25537  ioombl1lem4  25592  uniioombllem1  25612  uniioombllem2  25614  uniioombllem6  25619  mbfsup  25695  mbfinf  25696  mbflimsup  25697  itg2monolem1  25781  itg2mono  25784  ulm0  26420  pilem2  26481  pilem3  26482  ftalem3  27105  ftalem4  27106  ftalem5  27107  dchrabs  27290  pntlem3  27639  nocvxminlem  27813  bdayfinbndlem1  28526  tglnne0  28775  axlowdim1  29095  nvo00  30899  nmorepnf  30906  minvecolem1  31012  wrdpmtrlast  33223  cycpmco2lem5  33260  elrgspnlem1  33372  primefldchr  33434  fldgensdrg  33447  nsgqusf1olem1  33545  intlidl  33552  idlinsubrg  33563  rhmimaidl  33564  ssdifidl  33589  ssdifidlprm  33590  ssmxidl  33606  dflringlem2  33635  pidufd  33683  1arithufdlem1  33684  ply1dg1rtn0  33721  ply1degltlss  33736  exsslsb  33838  constrsdrg  34016  ordtconnlem1  34165  rrhre  34262  sigagenval  34381  oddpwdc  34595  bnj1177  35248  bnj1523  35313  rankfilimbi  35342  erdszelem8  35486  txsconnlem  35528  cvxsconn  35531  cvmsss2  35562  cvmliftmolem2  35570  cvmlift2lem12  35602  cvmliftpht  35606  finminlem  36616  onint1  36747  weiunlem  36761  weiunfr  36765  finxpreclem4  37826  heicant  38092  itg2addnc  38111  ftc1anclem7  38136  ftc1anc  38138  prdsbnd2  38232  lkrlss  39657  pclvalN  40452  dian0  41601  docaclN  41686  dicn0  41754  dihglblem5  41860  dihglb2  41904  doch2val2  41926  dochocss  41928  lclkr  42095  lclkrs  42101  lcfr  42147  aks6d1c6lem3  42727  unitscyglem2  42751  qsalrel  42795  nacsfix  43231  mzpcln0  43247  rencldnfilem  43335  fnwe2lem2  43566  kelac1  43578  harn0  43617  hbtlem2  43639  naddwordnexlem4  43916  omltoe  43921  gneispa  44644  imo72b2lem0  44679  scottrankd  44762  relpfrlem  45467  ubelsupr  45538  suprnmpt  45690  disjinfi  45708  suprubrnmpt2  45765  suprubrnmpt  45766  ssfiunibd  45826  allbutfi  45906  allbutfiinf  45932  uzn0d  45937  uzublem  45942  climinf  46120  limclr  46167  climinf2lem  46218  limsupubuzlem  46224  liminflelimsupuz  46297  cnrefiisplem  46341  ioodvbdlimc1lem1  46443  ioodvbdlimc1  46445  ioodvbdlimc2  46447  stoweidlem36  46548  fourierdlem20  46639  fourierdlem25  46644  fourierdlem31  46650  fourierdlem37  46656  fourierdlem46  46664  fourierdlem52  46670  fourierdlem54  46672  fouriercn  46744  elaa2lem  46745  salgenval  46833  salgenn0  46843  sge0isum  46939  sge0reuzb  46960  ovnlerp  47074  ovnf  47075  hsphoidmvle2  47097  hsphoidmvle  47098  hoiprodp1  47100  hoidmv1lelem1  47103  hoidmv1lelem3  47105  hoidmv1le  47106  hoidifhspdmvle  47132  hspmbllem1  47138  hspmbllem3  47140  ovnovollem2  47169  smflimlem1  47283  smfsuplem1  47323  smfsuplem3  47325  smflimsuplem5  47336  smflimsuplem7  47338  preimafvn0  47924  lincolss  48994  fvconstr2  49423  catprs  49570  discsubc  49623  iinfconstbas  49625  eloppf  49692  eloppf2  49693  oppcup3  49768  oppcthinendcALT  50000  termcterm3  50074  termcciso  50075  idfudiag1bas  50083  idfudiag1  50084