Theorem ne0d 4342

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

Syntax hints:   → wi 4   ∈ wcel 2108   ≠ wne 2940  ∅c0 4333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-dif 3954  df-nul 4334

This theorem is referenced by:  snnzg  4774  prnzg  4778  eqsnd  4830  exss  5468  isofrlem  7360  fvmpocurryd  8296  onnseq  8384  oeoalem  8634  oeoelem  8636  oeeui  8640  nnawordex  8675  omxpenlem  9113  frfi  9321  supgtoreq  9510  infltoreq  9542  cantnfp1lem2  9719  cantnfp1lem3  9720  oemapvali  9724  cantnflem1a  9725  cantnflem1d  9728  cantnflem1  9729  epfrs  9771  dfac9  10177  axdc3lem4  10493  intwun  10775  r1limwun  10776  gruina  10858  grur1a  10859  mulclpi  10933  indpi  10947  supsrlem  11151  axpre-sup  11209  supfirege  12255  uzn0  12895  suprzub  12981  fzn0  13578  flval3  13855  icopnfsup  13905  hashelne0d  14407  dfrtrcl2  15101  01sqrexlem3  15283  isercolllem2  15702  isercolllem3  15703  climsup  15706  mertenslem2  15921  gcdcllem1  16536  pclem  16876  prmreclem1  16954  4sqlem13  16995  vdwmc2  17017  vdwlem6  17024  vdwnnlem3  17035  prmgaplem3  17091  prmgaplem4  17092  mrcflem  17649  mrcval  17653  iscatd2  17724  mndbn0  18763  grpbn0  18984  issubgrpd2  19160  issubg4  19163  subgint  19168  nmzsubg  19183  cycsubgcl  19224  ghmpreima  19256  gastacl  19327  sylow1lem5  19620  pgpssslw  19632  sylow2alem2  19636  sylow2blem3  19640  fislw  19643  sylow3lem4  19648  torsubg  19872  oddvdssubg  19873  iscygd  19905  iscygodd  19906  dprdsubg  20044  ablfac1eu  20093  simpgnideld  20119  01eq0ring  20530  cntzsubrng  20567  cntzsubr  20606  imadrhmcl  20798  primefld  20806  primefld0cl  20807  primefld1cl  20808  abvn0b  20837  islss4  20960  lss1d  20961  lssintcl  20962  lspsolvlem  21144  lbsextlem1  21160  dflidl2rng  21228  lidlsubg  21233  rhmpreimaidl  21287  zringlpirlem1  21473  ocvlss  21690  lmiclbs  21857  lmisfree  21862  psrbas  21953  mplsubglem  22019  mplind  22094  mhpsubg  22157  mat1ric  22493  dmatsgrp  22505  scmatsgrp  22525  scmatsgrp1  22528  scmatlss  22531  scmatric  22543  cpmatsubgpmat  22726  matcpmric  22765  pmmpric  22829  clscld  23055  2ndcdisj  23464  dfac14lem  23625  opnfbas  23850  isfil2  23864  filn0  23870  filssufilg  23919  rnelfmlem  23960  flimfnfcls  24036  ptcmplem2  24061  clssubg  24117  tgpconncomp  24121  tsmsfbas  24136  ustfilxp  24221  ustne0  24222  xbln0  24424  bln0  24425  metustfbas  24570  metustbl  24579  nrgdomn  24692  icccmplem2  24845  icccmplem3  24846  reconnlem2  24849  phtpcer  25027  reparpht  25031  phtpcco2  25032  pcohtpy  25053  pcorevlem  25059  isclmp  25130  iscmet3lem2  25326  bcthlem4  25361  minveclem3b  25462  ivthlem2  25487  ivthlem3  25488  evthicc  25494  ovollb2  25524  ovolunlem1a  25531  ovolunlem1  25532  ovoliunlem1  25537  ovoliun2  25541  ioombl1lem4  25596  uniioombllem1  25616  uniioombllem2  25618  uniioombllem6  25623  mbfsup  25699  mbfinf  25700  mbflimsup  25701  itg2monolem1  25785  itg2mono  25788  ulm0  26434  pilem2  26496  pilem3  26497  ftalem3  27118  ftalem4  27119  ftalem5  27120  dchrabs  27304  pntlem3  27653  nocvxminlem  27822  tglnne0  28648  axlowdim1  28974  nvo00  30780  nmorepnf  30787  minvecolem1  30893  chnub  33002  submomnd  33087  wrdpmtrlast  33113  cycpmco2lem5  33150  elrgspnlem1  33246  primefldchr  33303  fldgensdrg  33316  suborng  33345  nsgqusf1olem1  33441  intlidl  33448  idlinsubrg  33459  rhmimaidl  33460  ssdifidl  33485  ssdifidlprm  33486  ssmxidl  33502  pidufd  33571  1arithufdlem1  33572  ply1dg1rtn0  33605  ply1degltlss  33617  exsslsb  33647  ordtconnlem1  33923  rrhre  34022  sigagenval  34141  oddpwdc  34356  bnj1177  35020  bnj1523  35085  erdszelem8  35203  txsconnlem  35245  cvxsconn  35248  cvmsss2  35279  cvmliftmolem2  35287  cvmlift2lem12  35319  cvmliftpht  35323  finminlem  36319  onint1  36450  weiunlem2  36464  weiunfr  36468  finxpreclem4  37395  heicant  37662  itg2addnc  37681  ftc1anclem7  37706  ftc1anc  37708  prdsbnd2  37802  lkrlss  39096  pclvalN  39892  dian0  41041  docaclN  41126  dicn0  41194  dihglblem5  41300  dihglb2  41344  doch2val2  41366  dochocss  41368  lclkr  41535  lclkrs  41541  lcfr  41587  aks6d1c6lem3  42173  unitscyglem2  42197  qsalrel  42281  nacsfix  42723  mzpcln0  42739  rencldnfilem  42831  fnwe2lem2  43063  kelac1  43075  harn0  43114  hbtlem2  43136  naddwordnexlem4  43414  omltoe  43420  gneispa  44143  imo72b2lem0  44178  scottrankd  44267  relpfrlem  44974  ubelsupr  45025  suprnmpt  45179  disjinfi  45197  suprubrnmpt2  45259  suprubrnmpt  45260  ssfiunibd  45321  allbutfi  45404  allbutfiinf  45431  uzn0d  45436  uzublem  45441  climinf  45621  limclr  45670  climinf2lem  45721  limsupubuzlem  45727  liminflelimsupuz  45800  cnrefiisplem  45844  ioodvbdlimc1lem1  45946  ioodvbdlimc1  45948  ioodvbdlimc2  45950  stoweidlem36  46051  fourierdlem20  46142  fourierdlem25  46147  fourierdlem31  46153  fourierdlem37  46159  fourierdlem46  46167  fourierdlem52  46173  fourierdlem54  46175  fouriercn  46247  elaa2lem  46248  salgenval  46336  salgenn0  46346  sge0isum  46442  sge0reuzb  46463  ovnlerp  46577  ovnf  46578  hsphoidmvle2  46600  hsphoidmvle  46601  hoiprodp1  46603  hoidmv1lelem1  46606  hoidmv1lelem3  46608  hoidmv1le  46609  hoidifhspdmvle  46635  hspmbllem1  46641  hspmbllem3  46643  ovnovollem2  46672  smflimlem1  46786  smfsuplem1  46826  smfsuplem3  46828  smflimsuplem5  46839  smflimsuplem7  46841  preimafvn0  47367  lincolss  48351  fvconstr2  48767  catprs  48900  oppcthinendcALT  49090  termcterm3  49147