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  7431  caseinr  7432  omniwomnimkv  7507  nninfdcinf  7511  acfun  7563  seq3val  10910  seqvalcd  10911  seqf1oglem2  10970  seqf1og  10971  hashennn  11233  wrdexg  11329  lswex  11370  ccatw2s1leng  11420  ccat2s1fvwd  11429  swrdspsleq  11453  cats1un  11507  cats1fvd  11552  s3fv0g  11577  s3fv1g  11578  s3fv2g  11579  s1s3d  11581  s1s4d  11582  s1s5d  11583  s1s6d  11584  s1s7d  11585  s2s2d  11586  s4s2d  11587  s4s3d  11588  s3s4d  11589  s2s5d  11590  s5s2d  11591  s4s4d  11592  lcmval  12857  ballotfilemsv  13302  ennnfonelemp1  13346  isstruct2r  13412  strnfvnd  13421  strfvssn  13423  strslfv2d  13444  setsslid  13452  basmex  13461  basmexd  13462  ressbas2d  13471  ressval3d  13475  imasival  13676  imasbas  13677  imasplusg  13678  imasmulr  13679  imasaddfn  13687  imasaddval  13688  imasaddf  13689  imasmulfn  13690  imasmulval  13691  imasmulf  13692  qusval  13693  qusaddflemg  13704  qusaddval  13705  qusaddf  13706  qusmulval  13707  qusmulf  13708  xpsfrnel  13714  ismgmn0  13727  gzsumvalx  13758  gzsumfzval  13760  gzsumval2  13763  ress0g  13805  ismhm  13817  mhmex  13818  0mhm  13842  qusgrp2  13965  mulgval  13974  mulgfng  13976  mulg1  13981  mulgnnp1  13982  mulgnndir  14003  issubg2m  14041  1nsgtrivd  14071  eqgval  14075  eqgen  14079  gsumvalfi  14201  prdsex  14221  prdsval  14222  prdsbaslemss  14223  prdssgrpd  14240  prdsidlem  14242  prdsmndd  14243  prds0g  14244  prdsgrpd  14246  prdsinvgd  14247  xpsval  14250  mgpplusg  14271  mgpbas  14274  rngpropd  14303  qusrng  14306  ringidval  14314  issrg  14318  ringidss  14383  ringpropd  14392  qusring2  14420  opprringb  14435  dvdsrvald  14449  dvdsrd  14450  isunitd  14462  invrfvald  14478  dvrfvald  14489  rdivmuldivd  14500  invrpropdg  14505  isrim0  14517  rhmunitinv  14534  subrgintm  14600  rrgmex  14618  aprval  14640  aprprop  14650  lssmex  14741  islss3  14765  sraval  14823  sralemg  14824  srascag  14828  sravscag  14829  sraipg  14830  sraex  14832  lidlmex  14861  lidlrsppropdg  14881  2idlmex  14887  qusrhm  14914  zrhval  15001  asclfval  15070  psrval  15099  psrbasg  15114  psrplusgg  15118  psraddcl  15120  psr0cl  15121  psr0lid  15122  psrnegcl  15123  psrlinv  15124  psrgrp  15125  psr1clfi  15128  mplsubgfilemcl  15139  istopon  15163  istps  15182  tgclb  15215  restbasg  15318  restco  15324  lmfval  15343  cnfval  15344  cnpfval  15345  cnpval  15348  txcnp  15421  txrest  15426  ismet2  15504  xmetpsmet  15519  mopnval  15592  comet  15649  reldvg  15829  dvmptclx  15868  lgseisenlem2  16288  1vgrex  16359  p1evtxdeqfilem  16650  p1evtxdeqfi  16651  p1evtxdp1fi  16652  upgriswlkdc  16699  eupth2lem3fi  16815  eupth2lembfi  16816