Theorem elexd 3460

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438

This theorem is referenced by:  ifexd  4525  rabexg  5276  reuhypd  5358  ideqg  5794  elrnmptg  5903  dmmptd  6627  elfvex  6858  fvmptd3f  6945  fvmptdv2  6948  tpres  7137  ovmpodxf  7499  ovmpodf  7505  mptmpoopabbrd  8015  mptmpoopabbrdOLD  8016  offval22  8021  mptsuppd  8120  suppssov1  8130  suppssov2  8131  suppssfv  8135  ordtypelem9  9418  cantnfp1lem2  9575  cantnflem3  9587  cnfcomlem  9595  ttukeylem3  10405  mptnn0fsupp  13904  mptnn0fsuppr  13906  seqf1olem2  13949  rtrclreclem1  14964  rtrclreclem2  14966  fsumrlim  15718  strfv2d  17112  prdsval  17359  imasval  17415  qusval  17446  xpsfrnel  17466  xpsval  17474  cofuval  17789  resfval  17799  funcres2c  17810  setcval  17984  catcval  18007  estrcval  18030  estrres  18045  xpcval  18083  prfval  18105  curfval  18129  uncfval  18140  isposd  18228  pospropd  18231  ipodrsima  18447  gsumvalx  18550  prdssgrpd  18607  prdsmndd  18644  prds0g  18645  prdsgrpd  18929  prdsinvgd  18930  eqgval  19056  prdscmnd  19740  isunit  20258  isirred  20304  isrim0  20368  rngcval  20503  ringcval  20532  prdslmodd  20872  frlmphllem  21687  psrval  21822  mvrfval  21888  opsrval  21951  selvffval  22018  mhpfval  22023  mhpmulcl  22034  psdffval  22042  evl1maprhm  22264  mamufval  22277  mvmulfval  22427  islocfin  23402  elmptrab2  23713  alexsub  23930  tsmsval2  24015  prdsdsf  24253  prdsxmet  24255  itg2gt0  25659  itgfsum  25726  mtest  26311  ssltd  27702  seqsp1  28210  mirval  28600  israg  28642  perpln1  28655  perpln2  28656  isperp  28657  midf  28721  ismidb  28723  lmif  28730  islmib  28732  f1otrg  28816  f1otrge  28817  structtocusgr  29391  iswlkg  29559  unidifsnne  32480  iinabrex  32513  funcnvmpt  32610  fdifsupp  32627  mgcoval  32928  fxpval  33107  elrgspnlem3  33184  rlocval  33199  subrdom  33224  fldgenval  33251  islbs5  33317  linds2eq  33318  elrspunidl  33365  resssra  33553  exsslsb  33563  irngval  33652  minplyval  33672  algextdeglem4  33687  constrextdg2lem  33715  constrext2chnlem  33717  rhmpreimacnlem  33851  ofcfval  34065  sitgval  34300  breprexplema  34598  lpadval  34644  bnj1463  35022  fineqvrep  35070  fineqvpow  35071  wevgblacfn  35082  wsuclem  35799  bj-inexeqex  37128  bj-idreseq  37136  bj-idreseqb  37137  bj-ideqg1ALT  37139  bj-imdirvallem  37154  opelopab3  37698  aks6d1c6lem2  42144  aks5lem2  42160  onsupex3  43207  pren2d  43529  frege81d  43720  frege129d  43736  rfovd  43974  fsovd  43981  fsovrfovd  43982  dssmapfvd  43990  rr-spce  44177  mnringvald  44186  grurankcld  44206  mnurnd  44256  dmmptdff  45201  dmmptdf2  45211  limsupequzmpt2  45699  liminfequzmpt2  45772  xlimliminflimsup  45843  rrxsnicc  46281  ioorrnopnlem  46285  ioorrnopnxrlem  46287  subsaliuncl  46339  sge0xaddlem1  46414  sge0xaddlem2  46415  sge0xadd  46416  sge0splitsn  46422  meaiininclem  46467  hoicvrrex  46537  ovn0lem  46546  hoidmvlelem3  46578  ovnhoilem1  46582  hoicoto2  46586  hoidifhspval3  46600  hoiqssbllem1  46603  ovolval4lem1  46630  vonvolmbl  46642  iinhoiicclem  46654  iunhoiioolem  46656  vonioolem1  46661  vonioolem2  46662  vonicclem1  46664  vonicclem2  46665  decsmf  46748  smflimlem4  46755  smfmullem4  46775  smfco  46783  smfpimcclem  46788  smflimsupmpt  46810  smfliminfmpt  46813  opabresex0d  47269  setsnidel  47361  isupwlkg  48121  isprsd  48939  initc  49076  funcoppc2  49128  swapfval  49247  fucofvalg  49303  prcofvalg  49361  lanfval  49598  ranfval  49599