Theorem elexd 3466

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

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3446

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448

This theorem is referenced by:  ifexd  4539  reuhypd  5379  ideqg  5812  elrnmptg  5919  dmmptd  6651  elfvex  6885  fvmptd3f  6968  fvmptdv2  6971  tpres  7155  ovmpodxf  7510  ovmpodf  7516  mptmpoopabbrd  8018  offval22  8025  mptsuppd  8123  suppssov1  8134  suppssfv  8138  ordtypelem9  9471  cantnfp1lem2  9624  cantnflem3  9636  cnfcomlem  9644  ttukeylem3  10456  mptnn0fsupp  13912  mptnn0fsuppr  13914  seqf1olem2  13958  rtrclreclem1  14954  rtrclreclem2  14956  fsumrlim  15707  strfv2d  17085  prdsval  17351  imasval  17407  qusval  17438  xpsfrnel  17458  xpsval  17466  cofuval  17782  resfval  17792  funcres2c  17802  setcval  17977  catcval  18000  estrcval  18025  estrres  18041  xpcval  18079  prfval  18101  curfval  18126  uncfval  18137  isposd  18226  pospropd  18230  ipodrsima  18444  gsumvalx  18545  prdsmndd  18603  prds0g  18604  prdsgrpd  18871  prdsinvgd  18872  eqgval  18993  prdscmnd  19653  isunit  20100  isirred  20144  isrim0  20172  prdslmodd  20487  frlmphllem  21223  psrval  21354  mvrfval  21426  opsrval  21484  selvffval  21563  mhpfval  21566  mhpmulcl  21576  mamufval  21771  mvmulfval  21928  islocfin  22905  elmptrab2  23216  alexsub  23433  tsmsval2  23518  prdsdsf  23757  prdsxmet  23759  itg2gt0  25162  itgfsum  25228  mtest  25800  ssltd  27174  mirval  27660  israg  27702  perpln1  27715  perpln2  27716  isperp  27717  midf  27781  ismidb  27783  lmif  27790  islmib  27792  f1otrg  27876  f1otrge  27877  structtocusgr  28457  iswlkg  28624  unidifsnne  31527  iinabrex  31554  funcnvmpt  31650  mgcoval  31916  fldgenval  32150  islbs5  32240  linds2eq  32241  elrspunidl  32279  irngval  32446  minplyval  32461  rhmpreimacnlem  32554  ofcfval  32786  sitgval  33021  breprexplema  33332  lpadval  33378  bnj1463  33756  fineqvrep  33785  fineqvpow  33786  wsuclem  34486  bj-inexeqex  35698  bj-idreseq  35706  bj-idreseqb  35707  bj-ideqg1ALT  35709  bj-imdirvallem  35724  opelopab3  36249  onsupex3  41626  pren2d  41950  frege81d  42141  frege129d  42157  rfovd  42395  fsovd  42402  fsovrfovd  42403  dssmapfvd  42411  rr-spce  42599  mnringvald  42610  grurankcld  42635  mnurnd  42685  dmmptdff  43565  dmmptdf2  43579  limsupequzmpt2  44079  limsupvaluz2  44099  liminfequzmpt2  44152  xlimliminflimsup  44223  rrxsnicc  44661  ioorrnopnlem  44665  ioorrnopnxrlem  44667  subsaliuncl  44719  sge0xaddlem1  44794  sge0xaddlem2  44795  sge0xadd  44796  sge0splitsn  44802  meaiininclem  44847  hoicvrrex  44917  ovn0lem  44926  hoidmvlelem3  44958  ovnhoilem1  44962  hoicoto2  44966  hoidifhspval3  44980  hoiqssbllem1  44983  ovolval4lem1  45010  vonvolmbl  45022  iinhoiicclem  45034  iunhoiioolem  45036  vonioolem1  45041  vonioolem2  45042  vonicclem1  45044  vonicclem2  45045  decsmf  45128  smflimlem4  45135  smfmullem4  45155  smfco  45163  smfpimcclem  45168  smflimsupmpt  45190  smfliminfmpt  45193  opabresex0d  45637  setsnidel  45689  isupwlkg  46159  rngcval  46380  ringcval  46426  isprsd  47108