Theorem elexd 3468

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3444

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 3446

This theorem is referenced by:  ifexd  4533  rabexg  5287  reuhypd  5369  ideqg  5805  elrnmptg  5914  dmmptd  6645  elfvex  6878  fvmptd3f  6965  fvmptdv2  6968  tpres  7157  ovmpodxf  7519  ovmpodf  7525  mptmpoopabbrd  8038  mptmpoopabbrdOLD  8039  offval22  8044  mptsuppd  8143  suppssov1  8153  suppssov2  8154  suppssfv  8158  ordtypelem9  9455  cantnfp1lem2  9608  cantnflem3  9620  cnfcomlem  9628  ttukeylem3  10440  mptnn0fsupp  13938  mptnn0fsuppr  13940  seqf1olem2  13983  rtrclreclem1  14999  rtrclreclem2  15001  fsumrlim  15753  strfv2d  17147  prdsval  17394  imasval  17450  qusval  17481  xpsfrnel  17501  xpsval  17509  cofuval  17820  resfval  17830  funcres2c  17841  setcval  18015  catcval  18038  estrcval  18061  estrres  18076  xpcval  18114  prfval  18136  curfval  18160  uncfval  18171  isposd  18259  pospropd  18262  ipodrsima  18476  gsumvalx  18579  prdssgrpd  18636  prdsmndd  18673  prds0g  18674  prdsgrpd  18958  prdsinvgd  18959  eqgval  19085  prdscmnd  19767  isunit  20258  isirred  20304  isrim0  20368  rngcval  20503  ringcval  20532  prdslmodd  20851  frlmphllem  21665  psrval  21800  mvrfval  21866  opsrval  21929  selvffval  21996  mhpfval  22001  mhpmulcl  22012  psdffval  22020  evl1maprhm  22242  mamufval  22255  mvmulfval  22405  islocfin  23380  elmptrab2  23691  alexsub  23908  tsmsval2  23993  prdsdsf  24231  prdsxmet  24233  itg2gt0  25637  itgfsum  25704  mtest  26289  ssltd  27679  seqsp1  28181  mirval  28558  israg  28600  perpln1  28613  perpln2  28614  isperp  28615  midf  28679  ismidb  28681  lmif  28688  islmib  28690  f1otrg  28774  f1otrge  28775  structtocusgr  29349  iswlkg  29517  unidifsnne  32438  iinabrex  32471  funcnvmpt  32564  fdifsupp  32581  mgcoval  32885  fxpval  33095  elrgspnlem3  33168  rlocval  33183  subrdom  33208  fldgenval  33235  islbs5  33324  linds2eq  33325  elrspunidl  33372  resssra  33556  exsslsb  33565  irngval  33653  minplyval  33668  algextdeglem4  33683  constrextdg2lem  33711  constrext2chnlem  33713  rhmpreimacnlem  33847  ofcfval  34061  sitgval  34296  breprexplema  34594  lpadval  34640  bnj1463  35018  fineqvrep  35058  fineqvpow  35059  wevgblacfn  35069  wsuclem  35786  bj-inexeqex  37115  bj-idreseq  37123  bj-idreseqb  37124  bj-ideqg1ALT  37126  bj-imdirvallem  37141  opelopab3  37685  aks6d1c6lem2  42132  aks5lem2  42148  onsupex3  43196  pren2d  43518  frege81d  43709  frege129d  43725  rfovd  43963  fsovd  43970  fsovrfovd  43971  dssmapfvd  43979  rr-spce  44166  mnringvald  44175  grurankcld  44195  mnurnd  44245  dmmptdff  45190  dmmptdf2  45200  limsupequzmpt2  45689  liminfequzmpt2  45762  xlimliminflimsup  45833  rrxsnicc  46271  ioorrnopnlem  46275  ioorrnopnxrlem  46277  subsaliuncl  46329  sge0xaddlem1  46404  sge0xaddlem2  46405  sge0xadd  46406  sge0splitsn  46412  meaiininclem  46457  hoicvrrex  46527  ovn0lem  46536  hoidmvlelem3  46568  ovnhoilem1  46572  hoicoto2  46576  hoidifhspval3  46590  hoiqssbllem1  46593  ovolval4lem1  46620  vonvolmbl  46632  iinhoiicclem  46644  iunhoiioolem  46646  vonioolem1  46651  vonioolem2  46652  vonicclem1  46654  vonicclem2  46655  decsmf  46738  smflimlem4  46745  smfmullem4  46765  smfco  46773  smfpimcclem  46778  smflimsupmpt  46800  smfliminfmpt  46803  opabresex0d  47259  setsnidel  47351  isupwlkg  48098  isprsd  48916  initc  49053  funcoppc2  49105  swapfval  49224  fucofvalg  49280  prcofvalg  49338  lanfval  49575  ranfval  49576