Theorem elexd 3460

Description: If a class is a member of another class, then it is a set. Deduction associated with elex 3457. (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 3457	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3436

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 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438

This theorem is referenced by:  ifexd  4519  rabexg  5270  reuhypd  5352  ideqg  5786  elrnmptg  5896  dmmptd  6621  elfvex  6852  fvmptd3f  6939  fvmptdv2  6942  tpres  7130  ovmpodxf  7491  ovmpodf  7497  mptmpoopabbrd  8007  mptmpoopabbrdOLD  8008  offval22  8013  mptsuppd  8112  suppssov1  8122  suppssov2  8123  suppssfv  8127  ordtypelem9  9407  cantnfp1lem2  9564  cantnflem3  9576  cnfcomlem  9584  ttukeylem3  10397  mptnn0fsupp  13899  mptnn0fsuppr  13901  seqf1olem2  13944  rtrclreclem1  14959  rtrclreclem2  14961  fsumrlim  15713  strfv2d  17107  prdsval  17354  imasval  17410  qusval  17441  xpsfrnel  17461  xpsval  17469  cofuval  17784  resfval  17794  funcres2c  17805  setcval  17979  catcval  18002  estrcval  18025  estrres  18040  xpcval  18078  prfval  18100  curfval  18124  uncfval  18135  isposd  18223  pospropd  18226  ipodrsima  18442  gsumvalx  18579  prdssgrpd  18636  prdsmndd  18673  prds0g  18674  prdsgrpd  18958  prdsinvgd  18959  eqgval  19084  prdscmnd  19768  isunit  20286  isirred  20332  isrim0  20395  rngcval  20528  ringcval  20557  prdslmodd  20897  frlmphllem  21712  psrval  21847  mvrfval  21913  opsrval  21976  selvffval  22043  mhpfval  22048  mhpmulcl  22059  psdffval  22067  evl1maprhm  22289  mamufval  22302  mvmulfval  22452  islocfin  23427  elmptrab2  23738  alexsub  23955  tsmsval2  24040  prdsdsf  24277  prdsxmet  24279  itg2gt0  25683  itgfsum  25750  mtest  26335  ssltd  27726  seqsp1  28236  mirval  28628  israg  28670  perpln1  28683  perpln2  28684  isperp  28685  midf  28749  ismidb  28751  lmif  28758  islmib  28760  f1otrg  28844  f1otrge  28845  structtocusgr  29419  iswlkg  29587  unidifsnne  32508  iinabrex  32541  funcnvmpt  32641  fdifsupp  32658  mgcoval  32959  fxpval  33126  elrgspnlem3  33203  rlocval  33218  subrdom  33243  fldgenval  33270  islbs5  33337  linds2eq  33338  elrspunidl  33385  splyval  33574  esplyval  33577  resssra  33591  exsslsb  33601  irngval  33690  minplyval  33710  algextdeglem4  33725  constrextdg2lem  33753  constrext2chnlem  33755  rhmpreimacnlem  33889  ofcfval  34103  sitgval  34337  breprexplema  34635  lpadval  34681  bnj1463  35059  fineqvrep  35129  fineqvpow  35130  fineqvnttrclse  35136  wevgblacfn  35145  wsuclem  35859  bj-inexeqex  37188  bj-idreseq  37196  bj-idreseqb  37197  bj-ideqg1ALT  37199  bj-imdirvallem  37214  opelopab3  37758  aks6d1c6lem2  42204  aks5lem2  42220  onsupex3  43267  pren2d  43589  frege81d  43780  frege129d  43796  rfovd  44034  fsovd  44041  fsovrfovd  44042  dssmapfvd  44050  rr-spce  44237  mnringvald  44246  grurankcld  44266  mnurnd  44316  dmmptdff  45260  dmmptdf2  45270  limsupequzmpt2  45756  liminfequzmpt2  45829  xlimliminflimsup  45900  rrxsnicc  46338  ioorrnopnlem  46342  ioorrnopnxrlem  46344  subsaliuncl  46396  sge0xaddlem1  46471  sge0xaddlem2  46472  sge0xadd  46473  sge0splitsn  46479  meaiininclem  46524  hoicvrrex  46594  ovn0lem  46603  hoidmvlelem3  46635  ovnhoilem1  46639  hoicoto2  46643  hoidifhspval3  46657  hoiqssbllem1  46660  ovolval4lem1  46687  vonvolmbl  46699  iinhoiicclem  46711  iunhoiioolem  46713  vonioolem1  46718  vonioolem2  46719  vonicclem1  46721  vonicclem2  46722  decsmf  46805  smflimlem4  46812  smfmullem4  46832  smfco  46840  smfpimcclem  46845  smflimsupmpt  46867  smfliminfmpt  46870  opabresex0d  47316  setsnidel  47408  isupwlkg  48168  isprsd  48986  initc  49123  funcoppc2  49175  swapfval  49294  fucofvalg  49350  prcofvalg  49408  lanfval  49645  ranfval  49646