Theorem elexd 3480

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Vcvv 3457

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459

This theorem is used by:  ifexd  4538  rabexg  5310  reuhypd  5392  ideqg  5839  elrnmptg  5953  dmmptd  6684  elfvex  6920  funcnvmpt  6995  fvmptd3f  7009  fvmptdv2  7012  tpres  7203  ovmpodxf  7566  ovmpodf  7572  mptmpoopabbrd  8080  offval22  8085  mptsuppd  8185  suppssov1  8195  suppssov2  8196  suppssfv  8200  ordtypelem9  9491  cantnfp1lem2  9651  cantnflem3  9663  cnfcomlem  9671  ttukeylem3  10506  mptnn0fsupp  14047  mptnn0fsuppr  14049  seqf1olem2  14092  rtrclreclem1  15114  rtrclreclem2  15116  fsumrlim  15882  strfv2d  17279  prdsval  17526  imasval  17583  qusval  17614  xpsfrnel  17634  xpsval  17642  cofuval  17957  resfval  17967  funcres2c  17978  setcval  18152  catcval  18175  estrcval  18198  estrres  18213  xpcval  18251  prfval  18273  curfval  18297  uncfval  18308  isposd  18396  pospropd  18399  ipodrsima  18615  gsumvalx  18756  prdssgrpd  18813  prdsmndd  18852  prds0g  18853  prdsgrpd  19140  prdsinvgd  19141  eqgval  19269  prdscmnd  19955  isunit  20481  isirred  20527  isrim0  20591  rngcval  20747  ringcval  20776  prdslmodd  21120  frlmphllem  21960  psrval  22095  mvrfval  22160  opsrval  22227  selvffval  22299  mhpfval  22331  mhpmulcl  22342  psdffval  22350  evl1maprhm  22569  mamufval  22579  mvmulfval  22729  islocfin  23705  elmptrab2  24016  alexsub  24233  tsmsval2  24318  prdsdsf  24555  prdsxmet  24557  itg2gt0  25950  itgfsum  26017  mtest  26598  sltsd  27992  seqsp1  28535  mirval  28963  israg  29008  perpln1  29021  perpln2  29022  isperp  29023  tgplnfn  29088  plngval  29090  isplng  29091  midf  29116  ismidb  29118  lmif  29125  islmib  29127  brprlng  29219  f1otrg  29251  f1otrge  29252  structtocusgr  29830  iswlkg  29997  unidifsnne  32929  iinabrex  32961  fdifsupp  33077  mgcoval  33346  fxpval  33525  elrgspnlem3  33604  rlocval  33619  subrdom  33645  fldgenval  33673  islbs5  33733  linds2eq  33734  elrspunidl  33776  0mplrim  33944  extvval  33961  splyval  33989  esplyval  33992  resssra  34017  exsslsb  34027  irngval  34115  minplyval  34135  algextdeglem4  34150  constrextdg2lem  34178  constrext2chnlem  34180  rhmpreimacnlem  34314  ofcfval  34528  sitgval  34763  breprexplema  35058  lpadval  35107  bnj1463  35484  fineqvrep  35560  fineqvpow  35561  fineqvnttrclse  35570  wevgblacfn  35628  wsuclem  36328  bj-inexeqex  37831  bj-idreseq  37839  bj-idreseqb  37840  bj-ideqg1ALT  37842  bj-imdirvallem  37857  opelopab3  38402  aks6d1c6lem2  42971  aks5lem2  42987  onsupex3  43994  pren2d  44315  frege81d  44506  frege129d  44522  rfovd  44760  fsovd  44767  fsovrfovd  44768  dssmapfvd  44776  rr-spce  44961  mnringvald  44970  grurankcld  44990  mnurnd  45026  dmmptdff  45972  dmmptdf2  45981  limsupequzmpt2  46465  liminfequzmpt2  46538  xlimliminflimsup  46609  rrxsnicc  47047  ioorrnopnlem  47051  ioorrnopnxrlem  47053  subsaliuncl  47105  sge0xaddlem1  47180  sge0xaddlem2  47181  sge0xadd  47182  sge0splitsn  47188  meaiininclem  47233  hoicvrrex  47303  ovn0lem  47312  hoidmvlelem3  47344  ovnhoilem1  47348  hoicoto2  47352  hoidifhspval3  47366  hoiqssbllem1  47369  ovolval4lem1  47396  vonvolmbl  47408  iinhoiicclem  47420  iunhoiioolem  47422  vonioolem1  47427  vonioolem2  47428  vonicclem1  47430  vonicclem2  47431  decsmf  47514  smflimlem4  47521  smfmullem4  47541  smfco  47549  smfpimcclem  47554  smflimsupmpt  47576  smfliminfmpt  47579  opabresex0d  48055  setsnidel  48159  isupwlkg  48935  isprsd  49766  initc  49902  funcoppc2  49954  swapfval  50073  fucofvalg  50129  prcofvalg  50187  lanfval  50424  ranfval  50425