Theorem elexd 3461

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

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439

This theorem is referenced by:  ifexd  4525  rabexg  5279  reuhypd  5361  ideqg  5797  elrnmptg  5907  dmmptd  6634  elfvex  6866  fvmptd3f  6953  fvmptdv2  6956  tpres  7144  ovmpodxf  7505  ovmpodf  7511  mptmpoopabbrd  8021  mptmpoopabbrdOLD  8022  offval22  8027  mptsuppd  8126  suppssov1  8136  suppssov2  8137  suppssfv  8141  ordtypelem9  9423  cantnfp1lem2  9580  cantnflem3  9592  cnfcomlem  9600  ttukeylem3  10413  mptnn0fsupp  13911  mptnn0fsuppr  13913  seqf1olem2  13956  rtrclreclem1  14971  rtrclreclem2  14973  fsumrlim  15725  strfv2d  17119  prdsval  17366  imasval  17423  qusval  17454  xpsfrnel  17474  xpsval  17482  cofuval  17797  resfval  17807  funcres2c  17818  setcval  17992  catcval  18015  estrcval  18038  estrres  18053  xpcval  18091  prfval  18113  curfval  18137  uncfval  18148  isposd  18236  pospropd  18239  ipodrsima  18455  gsumvalx  18592  prdssgrpd  18649  prdsmndd  18686  prds0g  18687  prdsgrpd  18971  prdsinvgd  18972  eqgval  19097  prdscmnd  19781  isunit  20300  isirred  20346  isrim0  20409  rngcval  20542  ringcval  20571  prdslmodd  20911  frlmphllem  21726  psrval  21862  mvrfval  21927  opsrval  21992  selvffval  22067  mhpfval  22072  mhpmulcl  22083  psdffval  22091  evl1maprhm  22314  mamufval  22327  mvmulfval  22477  islocfin  23452  elmptrab2  23763  alexsub  23980  tsmsval2  24065  prdsdsf  24302  prdsxmet  24304  itg2gt0  25708  itgfsum  25775  mtest  26360  ssltd  27751  seqsp1  28261  mirval  28653  israg  28695  perpln1  28708  perpln2  28709  isperp  28710  midf  28774  ismidb  28776  lmif  28783  islmib  28785  f1otrg  28869  f1otrge  28870  structtocusgr  29445  iswlkg  29613  unidifsnne  32537  iinabrex  32570  funcnvmpt  32671  fdifsupp  32690  mgcoval  32996  fxpval  33175  elrgspnlem3  33254  rlocval  33269  subrdom  33295  fldgenval  33322  islbs5  33389  linds2eq  33390  elrspunidl  33437  extvval  33624  splyval  33645  esplyval  33648  resssra  33671  exsslsb  33681  irngval  33770  minplyval  33790  algextdeglem4  33805  constrextdg2lem  33833  constrext2chnlem  33835  rhmpreimacnlem  33969  ofcfval  34183  sitgval  34417  breprexplema  34715  lpadval  34761  bnj1463  35139  fineqvrep  35209  fineqvpow  35210  fineqvnttrclse  35216  wevgblacfn  35225  wsuclem  35939  bj-inexeqex  37271  bj-idreseq  37279  bj-idreseqb  37280  bj-ideqg1ALT  37282  bj-imdirvallem  37297  opelopab3  37831  aks6d1c6lem2  42337  aks5lem2  42353  onsupex3  43391  pren2d  43713  frege81d  43904  frege129d  43920  rfovd  44158  fsovd  44165  fsovrfovd  44166  dssmapfvd  44174  rr-spce  44361  mnringvald  44370  grurankcld  44390  mnurnd  44440  dmmptdff  45383  dmmptdf2  45393  limsupequzmpt2  45878  liminfequzmpt2  45951  xlimliminflimsup  46022  rrxsnicc  46460  ioorrnopnlem  46464  ioorrnopnxrlem  46466  subsaliuncl  46518  sge0xaddlem1  46593  sge0xaddlem2  46594  sge0xadd  46595  sge0splitsn  46601  meaiininclem  46646  hoicvrrex  46716  ovn0lem  46725  hoidmvlelem3  46757  ovnhoilem1  46761  hoicoto2  46765  hoidifhspval3  46779  hoiqssbllem1  46782  ovolval4lem1  46809  vonvolmbl  46821  iinhoiicclem  46833  iunhoiioolem  46835  vonioolem1  46840  vonioolem2  46841  vonicclem1  46843  vonicclem2  46844  decsmf  46927  smflimlem4  46934  smfmullem4  46954  smfco  46962  smfpimcclem  46967  smflimsupmpt  46989  smfliminfmpt  46992  opabresex0d  47447  setsnidel  47539  isupwlkg  48299  isprsd  49116  initc  49252  funcoppc2  49304  swapfval  49423  fucofvalg  49479  prcofvalg  49537  lanfval  49774  ranfval  49775