Theorem elexd 3471

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3447

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 3449

This theorem is referenced by:  ifexd  4537  rabexg  5292  reuhypd  5374  ideqg  5815  elrnmptg  5925  dmmptd  6663  elfvex  6896  fvmptd3f  6983  fvmptdv2  6986  tpres  7175  ovmpodxf  7539  ovmpodf  7545  mptmpoopabbrd  8059  mptmpoopabbrdOLD  8060  offval22  8067  mptsuppd  8166  suppssov1  8176  suppssov2  8177  suppssfv  8181  ordtypelem9  9479  cantnfp1lem2  9632  cantnflem3  9644  cnfcomlem  9652  ttukeylem3  10464  mptnn0fsupp  13962  mptnn0fsuppr  13964  seqf1olem2  14007  rtrclreclem1  15023  rtrclreclem2  15025  fsumrlim  15777  strfv2d  17171  prdsval  17418  imasval  17474  qusval  17505  xpsfrnel  17525  xpsval  17533  cofuval  17844  resfval  17854  funcres2c  17865  setcval  18039  catcval  18062  estrcval  18085  estrres  18100  xpcval  18138  prfval  18160  curfval  18184  uncfval  18195  isposd  18283  pospropd  18286  ipodrsima  18500  gsumvalx  18603  prdssgrpd  18660  prdsmndd  18697  prds0g  18698  prdsgrpd  18982  prdsinvgd  18983  eqgval  19109  prdscmnd  19791  isunit  20282  isirred  20328  isrim0  20392  rngcval  20527  ringcval  20556  prdslmodd  20875  frlmphllem  21689  psrval  21824  mvrfval  21890  opsrval  21953  selvffval  22020  mhpfval  22025  mhpmulcl  22036  psdffval  22044  evl1maprhm  22266  mamufval  22279  mvmulfval  22429  islocfin  23404  elmptrab2  23715  alexsub  23932  tsmsval2  24017  prdsdsf  24255  prdsxmet  24257  itg2gt0  25661  itgfsum  25728  mtest  26313  ssltd  27703  seqsp1  28205  mirval  28582  israg  28624  perpln1  28637  perpln2  28638  isperp  28639  midf  28703  ismidb  28705  lmif  28712  islmib  28714  f1otrg  28798  f1otrge  28799  structtocusgr  29373  iswlkg  29541  unidifsnne  32465  iinabrex  32498  funcnvmpt  32591  fdifsupp  32608  mgcoval  32912  fxpval  33122  elrgspnlem3  33195  rlocval  33210  subrdom  33235  fldgenval  33262  islbs5  33351  linds2eq  33352  elrspunidl  33399  resssra  33583  exsslsb  33592  irngval  33680  minplyval  33695  algextdeglem4  33710  constrextdg2lem  33738  constrext2chnlem  33740  rhmpreimacnlem  33874  ofcfval  34088  sitgval  34323  breprexplema  34621  lpadval  34667  bnj1463  35045  fineqvrep  35085  fineqvpow  35086  wevgblacfn  35096  wsuclem  35813  bj-inexeqex  37142  bj-idreseq  37150  bj-idreseqb  37151  bj-ideqg1ALT  37153  bj-imdirvallem  37168  opelopab3  37712  aks6d1c6lem2  42159  aks5lem2  42175  onsupex3  43223  pren2d  43545  frege81d  43736  frege129d  43752  rfovd  43990  fsovd  43997  fsovrfovd  43998  dssmapfvd  44006  rr-spce  44193  mnringvald  44202  grurankcld  44222  mnurnd  44272  dmmptdff  45217  dmmptdf2  45227  limsupequzmpt2  45716  liminfequzmpt2  45789  xlimliminflimsup  45860  rrxsnicc  46298  ioorrnopnlem  46302  ioorrnopnxrlem  46304  subsaliuncl  46356  sge0xaddlem1  46431  sge0xaddlem2  46432  sge0xadd  46433  sge0splitsn  46439  meaiininclem  46484  hoicvrrex  46554  ovn0lem  46563  hoidmvlelem3  46595  ovnhoilem1  46599  hoicoto2  46603  hoidifhspval3  46617  hoiqssbllem1  46620  ovolval4lem1  46647  vonvolmbl  46659  iinhoiicclem  46671  iunhoiioolem  46673  vonioolem1  46678  vonioolem2  46679  vonicclem1  46681  vonicclem2  46682  decsmf  46765  smflimlem4  46772  smfmullem4  46792  smfco  46800  smfpimcclem  46805  smflimsupmpt  46827  smfliminfmpt  46830  opabresex0d  47286  setsnidel  47378  isupwlkg  48125  isprsd  48943  initc  49080  funcoppc2  49132  swapfval  49251  fucofvalg  49307  prcofvalg  49365  lanfval  49602  ranfval  49603