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  6616  tfrcllemsucfn  6629  frecrdg  6684  mapsnend  7105  mapunen  7157  unsnfidcel  7234  fnfi  7256  caseinl  7437  caseinr  7438  omniwomnimkv  7513  nninfdcinf  7517  acfun  7569  seq3val  10917  seqvalcd  10918  seqf1oglem2  10977  seqf1og  10978  hashennn  11240  wrdexg  11336  lswex  11377  ccatw2s1leng  11427  ccat2s1fvwd  11436  swrdspsleq  11460  cats1un  11514  cats1fvd  11559  s3fv0g  11584  s3fv1g  11585  s3fv2g  11586  s1s3d  11588  s1s4d  11589  s1s5d  11590  s1s6d  11591  s1s7d  11592  s2s2d  11593  s4s2d  11594  s4s3d  11595  s3s4d  11596  s2s5d  11597  s5s2d  11598  s4s4d  11599  lcmval  12865  ballotfilemsv  13310  ennnfonelemp1  13354  isstruct2r  13420  strnfvnd  13429  strfvssn  13431  strslfv2d  13452  setsslid  13460  basmex  13469  basmexd  13470  ressbas2d  13480  ressval3d  13484  imasival  13685  imasbas  13686  imasplusg  13687  imasmulr  13688  imasaddfn  13696  imasaddval  13697  imasaddf  13698  imasmulfn  13699  imasmulval  13700  imasmulf  13701  qusval  13702  qusaddflemg  13713  qusaddval  13714  qusaddf  13715  qusmulval  13716  qusmulf  13717  xpsfrnel  13723  ismgmn0  13736  gzsumvalx  13767  gzsumfzval  13769  gzsumval2  13772  ress0g  13814  ismhm  13826  mhmex  13827  0mhm  13851  qusgrp2  13974  mulgval  13983  mulgfng  13985  mulg1  13990  mulgnnp1  13991  mulgnndir  14012  issubg2m  14050  1nsgtrivd  14080  eqgval  14084  eqgen  14088  gsumvalfi  14241  prdsex  14278  prdsval  14279  prdsbaslemss  14280  prdssgrpd  14297  prdsidlem  14299  prdsmndd  14300  prds0g  14301  prdsgrpd  14303  prdsinvgd  14304  xpsval  14307  mgpplusg  14328  mgpbas  14331  rngpropd  14360  qusrng  14363  ringidval  14371  issrg  14375  ringidss  14440  ringpropd  14449  qusring2  14479  opprringb  14494  dvdsrvald  14508  dvdsrd  14509  isunitd  14521  invrfvald  14537  dvrfvald  14548  rdivmuldivd  14559  invrpropdg  14564  isrim0  14576  rhmunitinv  14593  subrgintm  14659  rrgmex  14677  aprval  14699  aprprop  14709  lssmex  14800  islss3  14824  sraval  14882  sralemg  14883  srascag  14887  sravscag  14888  sraipg  14889  sraex  14891  lidlmex  14920  lidlrsppropdg  14940  2idlmex  14946  qusrhm  14973  zrhval  15060  asclfval  15129  psrval  15160  psrbasg  15187  psrplusgg  15191  psraddcl  15193  psrmulrg  15195  psrmulclfilem  15198  psr0cl  15200  psr0lid  15201  psrnegcl  15202  psrlinv  15203  psrgrp  15204  psr1clfi  15207  psrlidmfi  15208  psrdifi  15211  psrdirfi  15212  mvrfval  15214  mvrval  15215  mvrval2  15216  mvrffi  15218  istopon  15256  istps  15275  tgclb  15308  restbasg  15411  restco  15417  lmfval  15436  cnfval  15437  cnpfval  15438  cnpval  15441  txcnp  15514  txrest  15519  ismet2  15597  xmetpsmet  15612  mopnval  15685  comet  15742  reldvg  15922  dvmptclx  15961  lgseisenlem2  16412  1vgrex  16483  p1evtxdeqfilem  16774  p1evtxdeqfi  16775  p1evtxdp1fi  16776  upgriswlkdc  16823  eupth2lem3fi  16939  eupth2lembfi  16940