Theorem elexd 3464

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442

This theorem is referenced by:  ifexd  4528  rabexg  5282  reuhypd  5364  ideqg  5800  elrnmptg  5910  dmmptd  6637  elfvex  6869  fvmptd3f  6956  fvmptdv2  6959  tpres  7147  ovmpodxf  7508  ovmpodf  7514  mptmpoopabbrd  8024  mptmpoopabbrdOLD  8025  offval22  8030  mptsuppd  8129  suppssov1  8139  suppssov2  8140  suppssfv  8144  ordtypelem9  9431  cantnfp1lem2  9588  cantnflem3  9600  cnfcomlem  9608  ttukeylem3  10421  mptnn0fsupp  13920  mptnn0fsuppr  13922  seqf1olem2  13965  rtrclreclem1  14980  rtrclreclem2  14982  fsumrlim  15734  strfv2d  17128  prdsval  17375  imasval  17432  qusval  17463  xpsfrnel  17483  xpsval  17491  cofuval  17806  resfval  17816  funcres2c  17827  setcval  18001  catcval  18024  estrcval  18047  estrres  18062  xpcval  18100  prfval  18122  curfval  18146  uncfval  18157  isposd  18245  pospropd  18248  ipodrsima  18464  gsumvalx  18601  prdssgrpd  18658  prdsmndd  18695  prds0g  18696  prdsgrpd  18980  prdsinvgd  18981  eqgval  19106  prdscmnd  19790  isunit  20309  isirred  20355  isrim0  20418  rngcval  20551  ringcval  20580  prdslmodd  20920  frlmphllem  21735  psrval  21871  mvrfval  21936  opsrval  22001  selvffval  22076  mhpfval  22081  mhpmulcl  22092  psdffval  22100  evl1maprhm  22323  mamufval  22336  mvmulfval  22486  islocfin  23461  elmptrab2  23772  alexsub  23989  tsmsval2  24074  prdsdsf  24311  prdsxmet  24313  itg2gt0  25717  itgfsum  25784  mtest  26369  sltsd  27764  seqsp1  28307  mirval  28727  israg  28769  perpln1  28782  perpln2  28783  isperp  28784  midf  28848  ismidb  28850  lmif  28857  islmib  28859  f1otrg  28943  f1otrge  28944  structtocusgr  29519  iswlkg  29687  unidifsnne  32611  iinabrex  32644  funcnvmpt  32745  fdifsupp  32764  mgcoval  33068  fxpval  33247  elrgspnlem3  33326  rlocval  33341  subrdom  33367  fldgenval  33394  islbs5  33461  linds2eq  33462  elrspunidl  33509  extvval  33696  splyval  33717  esplyval  33720  resssra  33743  exsslsb  33753  irngval  33842  minplyval  33862  algextdeglem4  33877  constrextdg2lem  33905  constrext2chnlem  33907  rhmpreimacnlem  34041  ofcfval  34255  sitgval  34489  breprexplema  34787  lpadval  34833  bnj1463  35211  fineqvrep  35270  fineqvpow  35271  fineqvnttrclse  35280  wevgblacfn  35303  wsuclem  36017  bj-inexeqex  37359  bj-idreseq  37367  bj-idreseqb  37368  bj-ideqg1ALT  37370  bj-imdirvallem  37385  opelopab3  37919  aks6d1c6lem2  42425  aks5lem2  42441  onsupex3  43476  pren2d  43797  frege81d  43988  frege129d  44004  rfovd  44242  fsovd  44249  fsovrfovd  44250  dssmapfvd  44258  rr-spce  44445  mnringvald  44454  grurankcld  44474  mnurnd  44524  dmmptdff  45467  dmmptdf2  45477  limsupequzmpt2  45962  liminfequzmpt2  46035  xlimliminflimsup  46106  rrxsnicc  46544  ioorrnopnlem  46548  ioorrnopnxrlem  46550  subsaliuncl  46602  sge0xaddlem1  46677  sge0xaddlem2  46678  sge0xadd  46679  sge0splitsn  46685  meaiininclem  46730  hoicvrrex  46800  ovn0lem  46809  hoidmvlelem3  46841  ovnhoilem1  46845  hoicoto2  46849  hoidifhspval3  46863  hoiqssbllem1  46866  ovolval4lem1  46893  vonvolmbl  46905  iinhoiicclem  46917  iunhoiioolem  46919  vonioolem1  46924  vonioolem2  46925  vonicclem1  46927  vonicclem2  46928  decsmf  47011  smflimlem4  47018  smfmullem4  47038  smfco  47046  smfpimcclem  47051  smflimsupmpt  47073  smfliminfmpt  47076  opabresex0d  47531  setsnidel  47623  isupwlkg  48383  isprsd  49200  initc  49336  funcoppc2  49388  swapfval  49507  fucofvalg  49563  prcofvalg  49621  lanfval  49858  ranfval  49859