Theorem elexd 3453

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435

This theorem is referenced by:  ifexd  4508  reuhypd  5343  ideqg  5763  elrnmptg  5871  dmmptd  6587  elfvex  6816  fvmptd3f  6899  fvmptdv2  6902  tpres  7085  ovmpodxf  7432  ovmpodf  7438  mptmpoopabbrd  7930  offval22  7937  mptsuppd  8012  suppssov1  8023  suppssfv  8027  ordtypelem9  9294  cantnfp1lem2  9446  cantnflem3  9458  cnfcomlem  9466  ttukeylem3  10276  mptnn0fsupp  13726  mptnn0fsuppr  13728  seqf1olem2  13772  rtrclreclem1  14777  rtrclreclem2  14779  fsumrlim  15532  strfv2d  16912  prdsval  17175  imasval  17231  qusval  17262  xpsfrnel  17282  xpsval  17290  cofuval  17606  resfval  17616  funcres2c  17626  setcval  17801  catcval  17824  estrcval  17849  estrres  17865  xpcval  17903  prfval  17925  curfval  17950  uncfval  17961  isposd  18050  pospropd  18054  ipodrsima  18268  gsumvalx  18369  prdsmndd  18427  prds0g  18428  prdsgrpd  18694  prdsinvgd  18695  eqgval  18814  prdscmnd  19471  isunit  19908  isirred  19950  prdslmodd  20240  frlmphllem  20996  psrval  21127  mvrfval  21198  opsrval  21256  selvffval  21335  mhpfval  21338  mhpmulcl  21348  mamufval  21543  mvmulfval  21700  islocfin  22677  elmptrab2  22988  alexsub  23205  tsmsval2  23290  prdsdsf  23529  prdsxmet  23531  itg2gt0  24934  itgfsum  25000  mtest  25572  mirval  27025  israg  27067  perpln1  27080  perpln2  27081  isperp  27082  midf  27146  ismidb  27148  lmif  27155  islmib  27157  f1otrg  27241  f1otrge  27242  structtocusgr  27822  iswlkg  27989  unidifsnne  30893  iinabrex  30917  funcnvmpt  31013  mgcoval  31273  linds2eq  31584  elrspunidl  31615  rhmpreimacnlem  31843  ofcfval  32075  sitgval  32308  breprexplema  32619  lpadval  32665  bnj1463  33044  fineqvrep  33073  fineqvpow  33074  wsuclem  33828  ssltd  33995  bj-inexeqex  35334  bj-idreseq  35342  bj-idreseqb  35343  bj-ideqg1ALT  35345  bj-imdirvallem  35360  opelopab3  35884  pren2d  41170  frege81d  41362  frege129d  41378  rfovd  41616  fsovd  41623  fsovrfovd  41624  dssmapfvd  41632  rr-spce  41822  mnringvald  41833  grurankcld  41858  mnurnd  41908  dmmptdf  42770  dmmptdf2  42783  limsupequzmpt2  43266  limsupvaluz2  43286  liminfequzmpt2  43339  xlimliminflimsup  43410  rrxsnicc  43848  ioorrnopnlem  43852  ioorrnopnxrlem  43854  subsaliuncl  43904  sge0xaddlem1  43978  sge0xaddlem2  43979  sge0xadd  43980  sge0splitsn  43986  meaiininclem  44031  hoicvrrex  44101  ovn0lem  44110  hoidmvlelem3  44142  ovnhoilem1  44146  hoicoto2  44150  hoidifhspval3  44164  hoiqssbllem1  44167  ovolval4lem1  44194  vonvolmbl  44206  iinhoiicclem  44218  iunhoiioolem  44220  vonioolem1  44225  vonioolem2  44226  vonicclem1  44228  vonicclem2  44229  decsmf  44312  smflimlem4  44319  smfmullem4  44339  smfco  44347  smfpimcclem  44351  smflimsupmpt  44373  smfliminfmpt  44376  opabresex0d  44788  setsnidel  44840  isupwlkg  45310  rngcval  45531  ringcval  45577  isprsd  46260