Theorem elexd 2835

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 2833	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  Vcvv 2821

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-v 2823

This theorem is used by:  ifexd  4632  dmmptd  5517  relndmfv  5731  mptsuppd  6500  suppssfvg  6507  tfr1onlemsucfn  6615  tfrcllemsucfn  6628  frecrdg  6683  mapsnend  7103  mapunen  7155  unsnfidcel  7232  fnfi  7254  caseinl  7437  caseinr  7438  omniwomnimkv  7513  nninfdcinf  7517  acfun  7569  seq3val  10918  seqvalcd  10919  seqf1oglem2  10978  seqf1og  10979  hashennn  11241  wrdexg  11337  lswex  11378  ccatw2s1leng  11428  ccat2s1fvwd  11437  swrdspsleq  11461  cats1un  11515  cats1fvd  11560  s3fv0g  11585  s3fv1g  11586  s3fv2g  11587  s1s3d  11589  s1s4d  11590  s1s5d  11591  s1s6d  11592  s1s7d  11593  s2s2d  11594  s4s2d  11595  s4s3d  11596  s3s4d  11597  s2s5d  11598  s5s2d  11599  s4s4d  11600  lcmval  12866  ballotfilemsv  13311  ennnfonelemp1  13355  isstruct2r  13421  strnfvnd  13430  strfvssn  13432  strslfv2d  13453  setsslid  13461  basmex  13470  basmexd  13471  ressbas2d  13481  ressval3d  13485  imasival  13686  imasbas  13687  imasplusg  13688  imasmulr  13689  imasaddfn  13697  imasaddval  13698  imasaddf  13699  imasmulfn  13700  imasmulval  13701  imasmulf  13702  qusval  13703  qusaddflemg  13714  qusaddval  13715  qusaddf  13716  qusmulval  13717  qusmulf  13718  xpsfrnel  13724  ismgmn0  13737  gzsumvalx  13768  gzsumfzval  13770  gzsumval2  13773  ress0g  13815  ismhm  13827  mhmex  13828  0mhm  13852  qusgrp2  13975  mulgval  13984  mulgfng  13986  mulg1  13991  mulgnnp1  13992  mulgnndir  14013  issubg2m  14051  1nsgtrivd  14081  eqgval  14085  eqgen  14089  gsumvalfi  14242  prdsex  14279  prdsval  14280  prdsbaslemss  14281  prdssgrpd  14298  prdsidlem  14300  prdsmndd  14301  prds0g  14302  prdsgrpd  14304  prdsinvgd  14305  xpsval  14308  mgpplusg  14329  mgpbas  14332  rngpropd  14361  qusrng  14364  ringidval  14372  issrg  14376  ringidss  14441  ringpropd  14450  qusring2  14480  opprringb  14495  dvdsrvald  14509  dvdsrd  14510  isunitd  14522  invrfvald  14538  dvrfvald  14549  rdivmuldivd  14560  invrpropdg  14565  isrim0  14577  rhmunitinv  14594  subrgintm  14660  rrgmex  14678  aprval  14700  aprprop  14710  lssmex  14801  islss3  14825  sraval  14883  sralemg  14884  srascag  14888  sravscag  14889  sraipg  14890  sraex  14892  lidlmex  14921  lidlrsppropdg  14941  2idlmex  14947  qusrhm  14974  zrhval  15061  asclfval  15130  psrval  15159  psrbasg  15178  psrplusgg  15182  psraddcl  15184  psrmulrg  15186  psrmulclfilem  15189  psr0cl  15191  psr0lid  15192  psrnegcl  15193  psrlinv  15194  psrgrp  15195  psr1clfi  15198  psrlidmfi  15199  psrdifi  15202  psrdirfi  15203  mplsubgfilemcl  15215  istopon  15239  istps  15258  tgclb  15291  restbasg  15394  restco  15400  lmfval  15419  cnfval  15420  cnpfval  15421  cnpval  15424  txcnp  15497  txrest  15502  ismet2  15580  xmetpsmet  15595  mopnval  15668  comet  15725  reldvg  15905  dvmptclx  15944  lgseisenlem2  16395  1vgrex  16466  p1evtxdeqfilem  16757  p1evtxdeqfi  16758  p1evtxdp1fi  16759  upgriswlkdc  16806  eupth2lem3fi  16922  eupth2lembfi  16923