Theorem elexd 3495

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

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3475

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477

This theorem is referenced by:  ifexd  4577  reuhypd  5418  ideqg  5852  elrnmptg  5959  dmmptd  6696  elfvex  6930  fvmptd3f  7014  fvmptdv2  7017  tpres  7202  ovmpodxf  7558  ovmpodf  7564  mptmpoopabbrd  8067  offval22  8074  mptsuppd  8172  suppssov1  8183  suppssfv  8187  ordtypelem9  9521  cantnfp1lem2  9674  cantnflem3  9686  cnfcomlem  9694  ttukeylem3  10506  mptnn0fsupp  13962  mptnn0fsuppr  13964  seqf1olem2  14008  rtrclreclem1  15004  rtrclreclem2  15006  fsumrlim  15757  strfv2d  17135  prdsval  17401  imasval  17457  qusval  17488  xpsfrnel  17508  xpsval  17516  cofuval  17832  resfval  17842  funcres2c  17852  setcval  18027  catcval  18050  estrcval  18075  estrres  18091  xpcval  18129  prfval  18151  curfval  18176  uncfval  18187  isposd  18276  pospropd  18280  ipodrsima  18494  gsumvalx  18595  prdssgrpd  18624  prdsmndd  18658  prds0g  18659  prdsgrpd  18933  prdsinvgd  18934  eqgval  19057  prdscmnd  19729  isunit  20187  isirred  20233  isrim0  20261  prdslmodd  20580  frlmphllem  21335  psrval  21468  mvrfval  21540  opsrval  21601  selvffval  21679  mhpfval  21682  mhpmulcl  21692  mamufval  21887  mvmulfval  22044  islocfin  23021  elmptrab2  23332  alexsub  23549  tsmsval2  23634  prdsdsf  23873  prdsxmet  23875  itg2gt0  25278  itgfsum  25344  mtest  25916  ssltd  27293  mirval  27906  israg  27948  perpln1  27961  perpln2  27962  isperp  27963  midf  28027  ismidb  28029  lmif  28036  islmib  28038  f1otrg  28122  f1otrge  28123  structtocusgr  28703  iswlkg  28870  unidifsnne  31773  iinabrex  31800  funcnvmpt  31892  mgcoval  32156  fldgenval  32402  islbs5  32496  linds2eq  32497  elrspunidl  32546  irngval  32749  minplyval  32766  algextdeglem1  32772  rhmpreimacnlem  32864  ofcfval  33096  sitgval  33331  breprexplema  33642  lpadval  33688  bnj1463  34066  fineqvrep  34095  fineqvpow  34096  wsuclem  34797  bj-inexeqex  36035  bj-idreseq  36043  bj-idreseqb  36044  bj-ideqg1ALT  36046  bj-imdirvallem  36061  opelopab3  36586  onsupex3  41983  pren2d  42307  frege81d  42498  frege129d  42514  rfovd  42752  fsovd  42759  fsovrfovd  42760  dssmapfvd  42768  rr-spce  42956  mnringvald  42967  grurankcld  42992  mnurnd  43042  dmmptdff  43922  dmmptdf2  43935  limsupequzmpt2  44434  limsupvaluz2  44454  liminfequzmpt2  44507  xlimliminflimsup  44578  rrxsnicc  45016  ioorrnopnlem  45020  ioorrnopnxrlem  45022  subsaliuncl  45074  sge0xaddlem1  45149  sge0xaddlem2  45150  sge0xadd  45151  sge0splitsn  45157  meaiininclem  45202  hoicvrrex  45272  ovn0lem  45281  hoidmvlelem3  45313  ovnhoilem1  45317  hoicoto2  45321  hoidifhspval3  45335  hoiqssbllem1  45338  ovolval4lem1  45365  vonvolmbl  45377  iinhoiicclem  45389  iunhoiioolem  45391  vonioolem1  45396  vonioolem2  45397  vonicclem1  45399  vonicclem2  45400  decsmf  45483  smflimlem4  45490  smfmullem4  45510  smfco  45518  smfpimcclem  45523  smflimsupmpt  45545  smfliminfmpt  45548  opabresex0d  45993  setsnidel  46045  isupwlkg  46515  rngcval  46860  ringcval  46906  isprsd  47588