Theorem elexd 3478

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

Syntax hints:   → wi 4   ∈ wcel 2143  Vcvv 3455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457

This theorem is referenced by:  ifexd  4536  rabexg  5308  reuhypd  5390  ideqg  5837  elrnmptg  5951  dmmptd  6680  elfvex  6916  funcnvmpt  6991  fvmptd3f  7005  fvmptdv2  7008  tpres  7199  ovmpodxf  7560  ovmpodf  7566  mptmpoopabbrd  8074  offval22  8079  mptsuppd  8179  suppssov1  8189  suppssov2  8190  suppssfv  8194  ordtypelem9  9484  cantnfp1lem2  9644  cantnflem3  9656  cnfcomlem  9664  ttukeylem3  10490  mptnn0fsupp  14029  mptnn0fsuppr  14031  seqf1olem2  14074  rtrclreclem1  15090  rtrclreclem2  15092  fsumrlim  15859  strfv2d  17256  prdsval  17503  imasval  17560  qusval  17591  xpsfrnel  17611  xpsval  17619  cofuval  17934  resfval  17944  funcres2c  17955  setcval  18129  catcval  18152  estrcval  18175  estrres  18190  xpcval  18228  prfval  18250  curfval  18274  uncfval  18285  isposd  18373  pospropd  18376  ipodrsima  18592  gsumvalx  18729  prdssgrpd  18786  prdsmndd  18823  prds0g  18824  prdsgrpd  19111  prdsinvgd  19112  eqgval  19240  prdscmnd  19926  isunit  20451  isirred  20497  isrim0  20561  rngcval  20717  ringcval  20746  prdslmodd  21090  frlmphllem  21930  psrval  22065  mvrfval  22130  opsrval  22197  selvffval  22269  mhpfval  22301  mhpmulcl  22312  psdffval  22320  evl1maprhm  22539  mamufval  22549  mvmulfval  22699  islocfin  23674  elmptrab2  23985  alexsub  24202  tsmsval2  24287  prdsdsf  24524  prdsxmet  24526  itg2gt0  25919  itgfsum  25986  mtest  26567  sltsd  27961  seqsp1  28504  mirval  28932  israg  28977  perpln1  28990  perpln2  28991  isperp  28992  tgplnfn  29057  plngval  29059  isplng  29060  midf  29085  ismidb  29087  lmif  29094  islmib  29096  brprlng  29188  f1otrg  29220  f1otrge  29221  structtocusgr  29796  iswlkg  29963  unidifsnne  32882  iinabrex  32914  fdifsupp  33030  mgcoval  33306  fxpval  33485  elrgspnlem3  33564  rlocval  33579  subrdom  33605  fldgenval  33633  islbs5  33693  linds2eq  33694  elrspunidl  33736  0mplrim  33904  extvval  33921  splyval  33949  esplyval  33952  resssra  33977  exsslsb  33987  irngval  34075  minplyval  34095  algextdeglem4  34110  constrextdg2lem  34138  constrext2chnlem  34140  rhmpreimacnlem  34274  ofcfval  34488  sitgval  34722  breprexplema  35017  lpadval  35066  bnj1463  35443  fineqvrep  35527  fineqvpow  35528  fineqvnttrclse  35537  wevgblacfn  35595  wsuclem  36315  bj-inexeqex  37798  bj-idreseq  37806  bj-idreseqb  37807  bj-ideqg1ALT  37809  bj-imdirvallem  37824  opelopab3  38369  aks6d1c6lem2  42938  aks5lem2  42954  onsupex3  43961  pren2d  44282  frege81d  44473  frege129d  44489  rfovd  44727  fsovd  44734  fsovrfovd  44735  dssmapfvd  44743  rr-spce  44928  mnringvald  44937  grurankcld  44957  mnurnd  44993  dmmptdff  45939  dmmptdf2  45948  limsupequzmpt2  46432  liminfequzmpt2  46505  xlimliminflimsup  46576  rrxsnicc  47014  ioorrnopnlem  47018  ioorrnopnxrlem  47020  subsaliuncl  47072  sge0xaddlem1  47147  sge0xaddlem2  47148  sge0xadd  47149  sge0splitsn  47155  meaiininclem  47200  hoicvrrex  47270  ovn0lem  47279  hoidmvlelem3  47311  ovnhoilem1  47315  hoicoto2  47319  hoidifhspval3  47333  hoiqssbllem1  47336  ovolval4lem1  47363  vonvolmbl  47375  iinhoiicclem  47387  iunhoiioolem  47389  vonioolem1  47394  vonioolem2  47395  vonicclem1  47397  vonicclem2  47398  decsmf  47481  smflimlem4  47488  smfmullem4  47508  smfco  47516  smfpimcclem  47521  smflimsupmpt  47543  smfliminfmpt  47546  opabresex0d  48022  setsnidel  48126  isupwlkg  48902  isprsd  49733  initc  49869  funcoppc2  49921  swapfval  50040  fucofvalg  50096  prcofvalg  50154  lanfval  50391  ranfval  50392