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  4630  dmmptd  5514  relndmfv  5728  mptsuppd  6496  suppssfvg  6503  tfr1onlemsucfn  6611  tfrcllemsucfn  6624  frecrdg  6679  mapsnend  7099  mapunen  7151  unsnfidcel  7228  fnfi  7250  caseinl  7432  caseinr  7433  omniwomnimkv  7508  nninfdcinf  7512  acfun  7564  seq3val  10912  seqvalcd  10913  seqf1oglem2  10972  seqf1og  10973  hashennn  11235  wrdexg  11331  lswex  11372  ccatw2s1leng  11422  ccat2s1fvwd  11431  swrdspsleq  11455  cats1un  11509  cats1fvd  11554  s3fv0g  11579  s3fv1g  11580  s3fv2g  11581  s1s3d  11583  s1s4d  11584  s1s5d  11585  s1s6d  11586  s1s7d  11587  s2s2d  11588  s4s2d  11589  s4s3d  11590  s3s4d  11591  s2s5d  11592  s5s2d  11593  s4s4d  11594  lcmval  12860  ballotfilemsv  13305  ennnfonelemp1  13349  isstruct2r  13415  strnfvnd  13424  strfvssn  13426  strslfv2d  13447  setsslid  13455  basmex  13464  basmexd  13465  ressbas2d  13475  ressval3d  13479  imasival  13680  imasbas  13681  imasplusg  13682  imasmulr  13683  imasaddfn  13691  imasaddval  13692  imasaddf  13693  imasmulfn  13694  imasmulval  13695  imasmulf  13696  qusval  13697  qusaddflemg  13708  qusaddval  13709  qusaddf  13710  qusmulval  13711  qusmulf  13712  xpsfrnel  13718  ismgmn0  13731  gzsumvalx  13762  gzsumfzval  13764  gzsumval2  13767  ress0g  13809  ismhm  13821  mhmex  13822  0mhm  13846  qusgrp2  13969  mulgval  13978  mulgfng  13980  mulg1  13985  mulgnnp1  13986  mulgnndir  14007  issubg2m  14045  1nsgtrivd  14075  eqgval  14079  eqgen  14083  gsumvalfi  14236  prdsex  14256  prdsval  14257  prdsbaslemss  14258  prdssgrpd  14275  prdsidlem  14277  prdsmndd  14278  prds0g  14279  prdsgrpd  14281  prdsinvgd  14282  xpsval  14285  mgpplusg  14306  mgpbas  14309  rngpropd  14338  qusrng  14341  ringidval  14349  issrg  14353  ringidss  14418  ringpropd  14427  qusring2  14455  opprringb  14470  dvdsrvald  14484  dvdsrd  14485  isunitd  14497  invrfvald  14513  dvrfvald  14524  rdivmuldivd  14535  invrpropdg  14540  isrim0  14552  rhmunitinv  14569  subrgintm  14635  rrgmex  14653  aprval  14675  aprprop  14685  lssmex  14776  islss3  14800  sraval  14858  sralemg  14859  srascag  14863  sravscag  14864  sraipg  14865  sraex  14867  lidlmex  14896  lidlrsppropdg  14916  2idlmex  14922  qusrhm  14949  zrhval  15036  asclfval  15105  psrval  15134  psrbasg  15150  psrplusgg  15154  psraddcl  15156  psrmulrg  15158  psrmulclfilem  15161  psr0cl  15163  psr0lid  15164  psrnegcl  15165  psrlinv  15166  psrgrp  15167  psr1clfi  15170  mplsubgfilemcl  15181  istopon  15205  istps  15224  tgclb  15257  restbasg  15360  restco  15366  lmfval  15385  cnfval  15386  cnpfval  15387  cnpval  15390  txcnp  15463  txrest  15468  ismet2  15546  xmetpsmet  15561  mopnval  15634  comet  15691  reldvg  15871  dvmptclx  15910  lgseisenlem2  16356  1vgrex  16427  p1evtxdeqfilem  16718  p1evtxdeqfi  16719  p1evtxdp1fi  16720  upgriswlkdc  16767  eupth2lem3fi  16883  eupth2lembfi  16884