Theorem ne0d 4335

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

Syntax hints:   → wi 4   ∈ wcel 2105   ≠ wne 2939  ∅c0 4322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-dif 3951  df-nul 4323

This theorem is referenced by:  snnzg  4778  prnzg  4782  exss  5463  isofrlem  7340  fvmpocurryd  8262  onnseq  8350  oeoalem  8602  oeoelem  8604  oeeui  8608  nnawordex  8643  omxpenlem  9079  frfi  9294  supgtoreq  9471  infltoreq  9503  cantnfp1lem2  9680  cantnfp1lem3  9681  oemapvali  9685  cantnflem1a  9686  cantnflem1d  9689  cantnflem1  9690  epfrs  9732  dfac9  10137  axdc3lem4  10454  intwun  10736  r1limwun  10737  gruina  10819  grur1a  10820  mulclpi  10894  indpi  10908  supsrlem  11112  axpre-sup  11170  supfirege  12208  uzn0  12846  suprzub  12930  fzn0  13522  flval3  13787  icopnfsup  13837  hashelne0d  14335  dfrtrcl2  15016  01sqrexlem3  15198  isercolllem2  15619  isercolllem3  15620  climsup  15623  mertenslem2  15838  gcdcllem1  16447  pclem  16778  prmreclem1  16856  4sqlem13  16897  vdwmc2  16919  vdwlem6  16926  vdwnnlem3  16937  prmgaplem3  16993  prmgaplem4  16994  mrcflem  17557  mrcval  17561  iscatd2  17632  mndbn0  18681  grpbn0  18894  issubgrpd2  19065  issubg4  19068  subgint  19073  nmzsubg  19088  cycsubgcl  19128  ghmpreima  19159  gastacl  19221  sylow1lem5  19518  pgpssslw  19530  sylow2alem2  19534  sylow2blem3  19538  fislw  19541  sylow3lem4  19546  torsubg  19770  oddvdssubg  19771  iscygd  19803  iscygodd  19804  dprdsubg  19942  ablfac1eu  19991  simpgnideld  20017  01eq0ring  20426  cntzsubrng  20463  cntzsubr  20504  imadrhmcl  20644  primefld  20652  primefld0cl  20653  primefld1cl  20654  islss4  20805  lss1d  20806  lssintcl  20807  lspsolvlem  20988  lbsextlem1  21004  lidlsubg  21075  dflidl2lem  21079  dflidl2rng  21118  abvn0b  21208  zringlpirlem1  21321  ocvlss  21534  lmiclbs  21701  lmisfree  21706  psrbas  21806  mplsubglem  21868  mplind  21941  mhpsubg  22004  mat1ric  22308  dmatsgrp  22320  scmatsgrp  22340  scmatsgrp1  22343  scmatlss  22346  scmatric  22358  cpmatsubgpmat  22541  matcpmric  22580  pmmpric  22644  clscld  22870  2ndcdisj  23279  dfac14lem  23440  opnfbas  23665  isfil2  23679  filn0  23685  filssufilg  23734  rnelfmlem  23775  flimfnfcls  23851  ptcmplem2  23876  clssubg  23932  tgpconncomp  23936  tsmsfbas  23951  ustfilxp  24036  ustne0  24037  xbln0  24239  bln0  24240  metustfbas  24385  metustbl  24394  nrgdomn  24507  icccmplem2  24658  icccmplem3  24659  reconnlem2  24662  phtpcer  24840  reparpht  24844  phtpcco2  24845  pcohtpy  24866  pcorevlem  24872  isclmp  24943  iscmet3lem2  25139  bcthlem4  25174  minveclem3b  25275  ivthlem2  25300  ivthlem3  25301  evthicc  25307  ovollb2  25337  ovolunlem1a  25344  ovolunlem1  25345  ovoliunlem1  25350  ovoliun2  25354  ioombl1lem4  25409  uniioombllem1  25429  uniioombllem2  25431  uniioombllem6  25436  mbfsup  25512  mbfinf  25513  mbflimsup  25514  itg2monolem1  25599  itg2mono  25602  ulm0  26241  pilem2  26303  pilem3  26304  ftalem3  26919  ftalem4  26920  ftalem5  26921  dchrabs  27105  pntlem3  27454  nocvxminlem  27622  tglnne0  28323  axlowdim1  28649  nvo00  30446  nmorepnf  30453  minvecolem1  30559  submomnd  32663  cycpmco2lem5  32724  primefldchr  32834  fldgensdrg  32839  suborng  32868  nsgqusf1olem1  32963  intlidl  32975  rhmpreimaidl  32976  idlinsubrg  32988  rhmimaidl  32989  ssmxidl  33029  ply1degltlss  33107  ordtconnlem1  33367  rrhre  33464  sigagenval  33601  oddpwdc  33816  bnj1177  34480  bnj1523  34545  erdszelem8  34652  txsconnlem  34694  cvxsconn  34697  cvmsss2  34728  cvmliftmolem2  34736  cvmlift2lem12  34768  cvmliftpht  34772  finminlem  35666  onint1  35797  finxpreclem4  36738  heicant  36986  itg2addnc  37005  ftc1anclem7  37030  ftc1anc  37032  prdsbnd2  37126  lkrlss  38428  pclvalN  39224  dian0  40373  docaclN  40458  dicn0  40526  dihglblem5  40632  dihglb2  40676  doch2val2  40698  dochocss  40700  lclkr  40867  lclkrs  40873  lcfr  40919  qsalrel  41528  nacsfix  41912  mzpcln0  41928  rencldnfilem  42020  fnwe2lem2  42255  kelac1  42267  harn0  42306  hbtlem2  42328  naddwordnexlem4  42614  omltoe  42620  gneispa  43343  scottrankd  43469  ubelsupr  44166  suprnmpt  44331  disjinfi  44349  suprubrnmpt2  44414  suprubrnmpt  44415  ssfiunibd  44477  allbutfi  44561  allbutfiinf  44588  uzn0d  44593  uzublem  44598  climinf  44780  limclr  44829  climinf2lem  44880  limsupubuzlem  44886  liminflelimsupuz  44959  cnrefiisplem  45003  ioodvbdlimc1lem1  45105  ioodvbdlimc1  45107  ioodvbdlimc2  45109  stoweidlem36  45210  fourierdlem20  45301  fourierdlem25  45306  fourierdlem31  45312  fourierdlem37  45318  fourierdlem46  45326  fourierdlem52  45332  fourierdlem54  45334  fouriercn  45406  elaa2lem  45407  salgenval  45495  salgenn0  45505  sge0isum  45601  sge0reuzb  45622  ovnlerp  45736  ovnf  45737  hsphoidmvle2  45759  hsphoidmvle  45760  hoiprodp1  45762  hoidmv1lelem1  45765  hoidmv1lelem3  45767  hoidmv1le  45768  hoidifhspdmvle  45794  hspmbllem1  45800  hspmbllem3  45802  ovnovollem2  45831  smflimlem1  45945  smfsuplem1  45985  smfsuplem3  45987  smflimsuplem5  45998  smflimsuplem7  46000  preimafvn0  46506  lincolss  47276  fvconstr2  47685  catprs  47792