Theorem elexd 3488

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3464

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466

This theorem is referenced by:  ifexd  4554  rabexg  5312  reuhypd  5394  ideqg  5836  elrnmptg  5946  dmmptd  6688  elfvex  6919  fvmptd3f  7006  fvmptdv2  7009  tpres  7198  ovmpodxf  7562  ovmpodf  7568  mptmpoopabbrd  8084  mptmpoopabbrdOLD  8085  offval22  8092  mptsuppd  8191  suppssov1  8201  suppssov2  8202  suppssfv  8206  ordtypelem9  9545  cantnfp1lem2  9698  cantnflem3  9710  cnfcomlem  9718  ttukeylem3  10530  mptnn0fsupp  14020  mptnn0fsuppr  14022  seqf1olem2  14065  rtrclreclem1  15081  rtrclreclem2  15083  fsumrlim  15832  strfv2d  17225  prdsval  17474  imasval  17530  qusval  17561  xpsfrnel  17581  xpsval  17589  cofuval  17900  resfval  17910  funcres2c  17921  setcval  18095  catcval  18118  estrcval  18141  estrres  18156  xpcval  18194  prfval  18216  curfval  18240  uncfval  18251  isposd  18339  pospropd  18342  ipodrsima  18556  gsumvalx  18659  prdssgrpd  18716  prdsmndd  18753  prds0g  18754  prdsgrpd  19038  prdsinvgd  19039  eqgval  19165  prdscmnd  19847  isunit  20338  isirred  20384  isrim0  20448  rngcval  20583  ringcval  20612  prdslmodd  20931  frlmphllem  21745  psrval  21880  mvrfval  21946  opsrval  22009  selvffval  22076  mhpfval  22081  mhpmulcl  22092  psdffval  22100  evl1maprhm  22322  mamufval  22335  mvmulfval  22485  islocfin  23460  elmptrab2  23771  alexsub  23988  tsmsval2  24073  prdsdsf  24311  prdsxmet  24313  itg2gt0  25718  itgfsum  25785  mtest  26370  ssltd  27760  seqsp1  28262  mirval  28639  israg  28681  perpln1  28694  perpln2  28695  isperp  28696  midf  28760  ismidb  28762  lmif  28769  islmib  28771  f1otrg  28855  f1otrge  28856  structtocusgr  29430  iswlkg  29598  unidifsnne  32522  iinabrex  32555  funcnvmpt  32650  fdifsupp  32667  mgcoval  32971  elrgspnlem3  33244  rlocval  33259  subrdom  33284  fldgenval  33311  islbs5  33400  linds2eq  33401  elrspunidl  33448  resssra  33632  exsslsb  33641  irngval  33731  minplyval  33744  algextdeglem4  33759  constrextdg2lem  33787  constrext2chnlem  33789  rhmpreimacnlem  33920  ofcfval  34134  sitgval  34369  breprexplema  34667  lpadval  34713  bnj1463  35091  fineqvrep  35131  fineqvpow  35132  wevgblacfn  35136  wsuclem  35848  bj-inexeqex  37177  bj-idreseq  37185  bj-idreseqb  37186  bj-ideqg1ALT  37188  bj-imdirvallem  37203  opelopab3  37747  aks6d1c6lem2  42189  aks5lem2  42205  onsupex3  43233  pren2d  43555  frege81d  43746  frege129d  43762  rfovd  44000  fsovd  44007  fsovrfovd  44008  dssmapfvd  44016  rr-spce  44203  mnringvald  44212  grurankcld  44232  mnurnd  44282  dmmptdff  45227  dmmptdf2  45237  limsupequzmpt2  45727  liminfequzmpt2  45800  xlimliminflimsup  45871  rrxsnicc  46309  ioorrnopnlem  46313  ioorrnopnxrlem  46315  subsaliuncl  46367  sge0xaddlem1  46442  sge0xaddlem2  46443  sge0xadd  46444  sge0splitsn  46450  meaiininclem  46495  hoicvrrex  46565  ovn0lem  46574  hoidmvlelem3  46606  ovnhoilem1  46610  hoicoto2  46614  hoidifhspval3  46628  hoiqssbllem1  46631  ovolval4lem1  46658  vonvolmbl  46670  iinhoiicclem  46682  iunhoiioolem  46684  vonioolem1  46689  vonioolem2  46690  vonicclem1  46692  vonicclem2  46693  decsmf  46776  smflimlem4  46783  smfmullem4  46803  smfco  46811  smfpimcclem  46816  smflimsupmpt  46838  smfliminfmpt  46841  opabresex0d  47294  setsnidel  47371  isupwlkg  48092  isprsd  48909  funcoppc2  49066  swapfval  49159  fucofvalg  49209  prcofvalg  49267  lanfval  49470  ranfval  49471