Theorem elexd 3461

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

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443

This theorem is referenced by:  reuhypd  5285  ideqg  5686  elrnmptg  5795  dmmptd  6465  elfvex  6678  fvmptd3f  6760  fvmptdv2  6763  fmptpr  6911  tpres  6940  ovmpodxf  7279  ovmpodf  7285  offval22  7766  mptsuppd  7836  suppssov1  7845  suppssfv  7849  oeeu  8212  mapsnend  8571  cantnfp1lem2  9126  cantnflem3  9138  oef1o  9145  cnfcomlem  9146  pm54.43lem  9413  ttukeylem3  9922  mptnn0fsupp  13360  mptnn0fsuppr  13362  seqf1olem2  13406  hashbclem  13806  rtrclreclem1  14408  rtrclreclem2  14410  fsumrlim  15158  strfv2d  16521  prdsval  16720  imasval  16776  qusval  16807  xpsfrnel  16827  xpsval  16835  cofuval  17144  resfval  17154  funcres2c  17163  setcval  17329  catcval  17348  estrcval  17366  estrres  17381  xpcval  17419  prfval  17441  curfval  17465  uncfval  17476  isposd  17557  pospropd  17736  ipodrsima  17767  gsumvalx  17878  prdsmndd  17936  prds0g  17937  prdsgrpd  18201  prdsinvgd  18202  eqgval  18321  prdscmnd  18974  isunit  19403  isirred  19445  issrng  19614  prdslmodd  19734  frlmphllem  20469  psrval  20600  mvrfval  20658  opsrval  20714  selvffval  20788  mhpfval  20791  mamufval  20992  mvmulfval  21147  islocfin  22122  elmptrab2  22433  alexsub  22650  tsmsval2  22735  prdsdsf  22974  prdsxmet  22976  itg2gt0  24364  itgfsum  24430  mtest  24999  mirval  26449  israg  26491  perpln1  26504  perpln2  26505  isperp  26506  midf  26570  ismidb  26572  lmif  26579  islmib  26581  f1otrg  26665  f1otrge  26666  structtocusgr  27236  1loopgrnb0  27292  iswlkg  27403  unidifsnne  30308  iinabrex  30332  funcnvmpt  30430  mgcoval  30694  linds2eq  30995  elrspunidl  31014  rhmpreimacnlem  31237  ofcfval  31467  sitgval  31700  breprexplema  32011  lpadval  32057  bnj1463  32437  wsuclem  33225  bj-inexeqex  34569  bj-idreseq  34577  bj-idreseqb  34578  bj-ideqg1ALT  34580  bj-imdirvallem  34595  opelopab3  35155  pren2d  40255  frege81d  40448  frege129d  40464  rfovd  40702  fsovd  40709  fsovrfovd  40710  dssmapfvd  40718  rr-spce  40910  mnringvald  40921  grurankcld  40941  mnurnd  40991  dmmptdf  41854  dmmptdf2  41869  limsupvaluz  42350  limsupequzmpt2  42360  limsupvaluz2  42380  liminfequzmpt2  42433  xlimliminflimsup  42504  rrxsnicc  42942  ioorrnopnlem  42946  ioorrnopnxrlem  42948  subsaliuncl  42998  sge0xaddlem1  43072  sge0xaddlem2  43073  sge0xadd  43074  sge0splitsn  43080  meaiininclem  43125  hoicvrrex  43195  ovn0lem  43204  hoidmvlelem3  43236  ovnhoilem1  43240  hoicoto2  43244  hoidifhspval3  43258  hoiqssbllem1  43261  ovolval4lem1  43288  vonvolmbl  43300  iinhoiicclem  43312  iunhoiioolem  43314  vonioolem1  43319  vonioolem2  43320  vonicclem1  43322  vonicclem2  43323  decsmf  43400  smflimlem4  43407  smfmullem4  43426  smfco  43434  smfpimcclem  43438  smflimsupmpt  43460  smfliminfmpt  43463  opabresex0d  43841  setsnidel  43894  isupwlkg  44365  rngcval  44586  ringcval  44632