Theorem elexd 3476

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

Syntax hints:   → wi 4   ∈ wcel 2141  Vcvv 3453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455

This theorem is referenced by:  ifexd  4526  rabexg  5290  reuhypd  5373  ideqg  5819  elrnmptg  5933  dmmptd  6661  elfvex  6897  funcnvmpt  6972  fvmptd3f  6986  fvmptdv2  6989  tpres  7180  ovmpodxf  7541  ovmpodf  7547  mptmpoopabbrd  8056  offval22  8061  mptsuppd  8161  suppssov1  8171  suppssov2  8172  suppssfv  8176  ordtypelem9  9468  cantnfp1lem2  9628  cantnflem3  9640  cnfcomlem  9648  ttukeylem3  10462  mptnn0fsupp  14004  mptnn0fsuppr  14006  seqf1olem2  14049  rtrclreclem1  15064  rtrclreclem2  15066  fsumrlim  15830  strfv2d  17228  prdsval  17475  imasval  17532  qusval  17563  xpsfrnel  17583  xpsval  17591  cofuval  17906  resfval  17916  funcres2c  17927  setcval  18101  catcval  18124  estrcval  18147  estrres  18162  xpcval  18200  prfval  18222  curfval  18246  uncfval  18257  isposd  18345  pospropd  18348  ipodrsima  18564  gsumvalx  18701  prdssgrpd  18758  prdsmndd  18795  prds0g  18796  prdsgrpd  19083  prdsinvgd  19084  eqgval  19209  prdscmnd  19892  isunit  20409  isirred  20455  isrim0  20518  rngcval  20655  ringcval  20684  prdslmodd  21024  frlmphllem  21820  psrval  21955  mvrfval  22020  opsrval  22087  selvffval  22159  mhpfval  22191  mhpmulcl  22202  psdffval  22210  evl1maprhm  22430  mamufval  22440  mvmulfval  22590  islocfin  23565  elmptrab2  23876  alexsub  24093  tsmsval2  24178  prdsdsf  24415  prdsxmet  24417  itg2gt0  25810  itgfsum  25877  mtest  26455  sltsd  27849  seqsp1  28392  mirval  28812  israg  28854  perpln1  28867  perpln2  28868  isperp  28869  midf  28933  ismidb  28935  lmif  28942  islmib  28944  f1otrg  29028  f1otrge  29029  structtocusgr  29604  iswlkg  29771  unidifsnne  32695  iinabrex  32729  fdifsupp  32848  mgcoval  33125  fxpval  33306  elrgspnlem3  33386  rlocval  33401  subrdom  33430  fldgenval  33460  islbs5  33527  linds2eq  33528  elrspunidl  33575  0mplrim  33772  extvval  33789  splyval  33817  esplyval  33820  resssra  33845  exsslsb  33855  irngval  33943  minplyval  33963  algextdeglem4  33978  constrextdg2lem  34006  constrext2chnlem  34008  rhmpreimacnlem  34142  ofcfval  34356  sitgval  34590  breprexplema  34885  lpadval  34934  bnj1463  35311  fineqvrep  35371  fineqvpow  35372  fineqvnttrclse  35381  wevgblacfn  35415  wsuclem  36134  bj-inexeqex  37607  bj-idreseq  37615  bj-idreseqb  37616  bj-ideqg1ALT  37618  bj-imdirvallem  37633  opelopab3  38178  aks6d1c6lem2  42749  aks5lem2  42765  onsupex3  43772  pren2d  44093  frege81d  44284  frege129d  44300  rfovd  44538  fsovd  44545  fsovrfovd  44546  dssmapfvd  44554  rr-spce  44741  mnringvald  44750  grurankcld  44770  mnurnd  44820  dmmptdff  45760  dmmptdf2  45769  limsupequzmpt2  46253  liminfequzmpt2  46326  xlimliminflimsup  46397  rrxsnicc  46835  ioorrnopnlem  46839  ioorrnopnxrlem  46841  subsaliuncl  46893  sge0xaddlem1  46968  sge0xaddlem2  46969  sge0xadd  46970  sge0splitsn  46976  meaiininclem  47021  hoicvrrex  47091  ovn0lem  47100  hoidmvlelem3  47132  ovnhoilem1  47136  hoicoto2  47140  hoidifhspval3  47154  hoiqssbllem1  47157  ovolval4lem1  47184  vonvolmbl  47196  iinhoiicclem  47208  iunhoiioolem  47210  vonioolem1  47215  vonioolem2  47216  vonicclem1  47218  vonicclem2  47219  decsmf  47302  smflimlem4  47309  smfmullem4  47329  smfco  47337  smfpimcclem  47342  smflimsupmpt  47364  smfliminfmpt  47367  opabresex0d  47840  setsnidel  47944  isupwlkg  48720  isprsd  49537  initc  49673  funcoppc2  49725  swapfval  49844  fucofvalg  49900  prcofvalg  49958  lanfval  50195  ranfval  50196