Theorem elexd 2776

Description: If a class is a member of another class, it is a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.)

Hypothesis

Ref	Expression
elexd.1	⊢ (𝜑 → 𝐴 ∈ 𝑉)

Assertion

Ref	Expression
elexd	⊢ (𝜑 → 𝐴 ∈ V)

Proof of Theorem elexd

Step	Hyp	Ref	Expression
1		elexd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		elex 2774	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2167  Vcvv 2763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-v 2765

This theorem is referenced by:  ifexd  4519  dmmptd  5388  tfr1onlemsucfn  6398  tfrcllemsucfn  6411  frecrdg  6466  unsnfidcel  6982  fnfi  7002  caseinl  7157  caseinr  7158  omniwomnimkv  7233  nninfdcinf  7237  acfun  7274  seq3val  10552  seqvalcd  10553  seqf1oglem2  10612  seqf1og  10613  hashennn  10872  wrdexg  10946  lcmval  12231  hashdvds  12389  ennnfonelemp1  12623  isstruct2r  12689  strnfvnd  12698  strfvssn  12700  strslfv2d  12721  setsslid  12729  basmex  12737  basmexd  12738  ressbas2d  12746  ressval3d  12750  prdsex  12940  imasival  12949  imasbas  12950  imasplusg  12951  imasmulr  12952  imasaddfn  12960  imasaddval  12961  imasaddf  12962  imasmulfn  12963  imasmulval  12964  imasmulf  12965  qusval  12966  qusaddflemg  12977  qusaddval  12978  qusaddf  12979  qusmulval  12980  qusmulf  12981  xpsfrnel  12987  xpsval  12995  ismgmn0  13001  igsumvalx  13032  gsumfzval  13034  gsumval2  13040  ress0g  13084  ismhm  13093  mhmex  13094  0mhm  13118  qusgrp2  13243  mulgval  13252  mulgfng  13254  mulg1  13259  mulgnnp1  13260  mulgnndir  13281  issubg2m  13319  1nsgtrivd  13349  eqgval  13353  eqgen  13357  rngpropd  13511  qusrng  13514  issrg  13521  ringidss  13585  ringpropd  13594  qusring2  13622  dvdsrvald  13649  dvdsrd  13650  isunitd  13662  invrfvald  13678  dvrfvald  13689  rdivmuldivd  13700  invrpropdg  13705  isrim0  13717  rhmunitinv  13734  subrgintm  13799  rrgmex  13817  aprval  13838  lssmex  13911  islss3  13935  sraval  13993  sralemg  13994  srascag  13998  sravscag  13999  sraipg  14000  sraex  14002  lidlmex  14031  lidlrsppropdg  14051  2idlmex  14057  qusrhm  14084  zrhval  14173  psrval  14220  psrbasg  14227  psrplusgg  14230  psraddcl  14232  istopon  14249  istps  14268  tgclb  14301  restbasg  14404  restco  14410  lmfval  14428  cnfval  14430  cnpfval  14431  cnpval  14434  txcnp  14507  txrest  14512  ismet2  14590  xmetpsmet  14605  mopnval  14678  comet  14735  reldvg  14915  dvmptclx  14954  lgseisenlem2  15312