Theorem elexd 3453

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431

This theorem is referenced by:  ifexd  4515  rabexg  5278  reuhypd  5361  ideqg  5806  elrnmptg  5916  dmmptd  6643  elfvex  6875  funcnvmpt  6949  fvmptd3f  6963  fvmptdv2  6966  tpres  7156  ovmpodxf  7517  ovmpodf  7523  mptmpoopabbrd  8033  offval22  8038  mptsuppd  8137  suppssov1  8147  suppssov2  8148  suppssfv  8152  ordtypelem9  9441  cantnfp1lem2  9600  cantnflem3  9612  cnfcomlem  9620  ttukeylem3  10433  mptnn0fsupp  13959  mptnn0fsuppr  13961  seqf1olem2  14004  rtrclreclem1  15019  rtrclreclem2  15021  fsumrlim  15774  strfv2d  17171  prdsval  17418  imasval  17475  qusval  17506  xpsfrnel  17526  xpsval  17534  cofuval  17849  resfval  17859  funcres2c  17870  setcval  18044  catcval  18067  estrcval  18090  estrres  18105  xpcval  18143  prfval  18165  curfval  18189  uncfval  18200  isposd  18288  pospropd  18291  ipodrsima  18507  gsumvalx  18644  prdssgrpd  18701  prdsmndd  18738  prds0g  18739  prdsgrpd  19026  prdsinvgd  19027  eqgval  19152  prdscmnd  19836  isunit  20353  isirred  20399  isrim0  20462  rngcval  20595  ringcval  20624  prdslmodd  20964  frlmphllem  21760  psrval  21895  mvrfval  21959  opsrval  22024  selvffval  22099  mhpfval  22104  mhpmulcl  22115  psdffval  22123  evl1maprhm  22344  mamufval  22357  mvmulfval  22507  islocfin  23482  elmptrab2  23793  alexsub  24010  tsmsval2  24095  prdsdsf  24332  prdsxmet  24334  itg2gt0  25727  itgfsum  25794  mtest  26369  sltsd  27760  seqsp1  28303  mirval  28723  israg  28765  perpln1  28778  perpln2  28779  isperp  28780  midf  28844  ismidb  28846  lmif  28853  islmib  28855  f1otrg  28939  f1otrge  28940  structtocusgr  29515  iswlkg  29682  unidifsnne  32606  iinabrex  32639  fdifsupp  32758  mgcoval  33046  fxpval  33226  elrgspnlem3  33305  rlocval  33320  subrdom  33346  fldgenval  33373  islbs5  33440  linds2eq  33441  elrspunidl  33488  extvval  33675  splyval  33703  esplyval  33706  resssra  33731  exsslsb  33741  irngval  33829  minplyval  33849  algextdeglem4  33864  constrextdg2lem  33892  constrext2chnlem  33894  rhmpreimacnlem  34028  ofcfval  34242  sitgval  34476  breprexplema  34774  lpadval  34820  bnj1463  35197  fineqvrep  35258  fineqvpow  35259  fineqvnttrclse  35268  wevgblacfn  35291  wsuclem  36005  bj-inexeqex  37468  bj-idreseq  37476  bj-idreseqb  37477  bj-ideqg1ALT  37479  bj-imdirvallem  37494  opelopab3  38039  aks6d1c6lem2  42610  aks5lem2  42626  onsupex3  43662  pren2d  43983  frege81d  44174  frege129d  44190  rfovd  44428  fsovd  44435  fsovrfovd  44436  dssmapfvd  44444  rr-spce  44631  mnringvald  44640  grurankcld  44660  mnurnd  44710  dmmptdff  45652  dmmptdf2  45662  limsupequzmpt2  46146  liminfequzmpt2  46219  xlimliminflimsup  46290  rrxsnicc  46728  ioorrnopnlem  46732  ioorrnopnxrlem  46734  subsaliuncl  46786  sge0xaddlem1  46861  sge0xaddlem2  46862  sge0xadd  46863  sge0splitsn  46869  meaiininclem  46914  hoicvrrex  46984  ovn0lem  46993  hoidmvlelem3  47025  ovnhoilem1  47029  hoicoto2  47033  hoidifhspval3  47047  hoiqssbllem1  47050  ovolval4lem1  47077  vonvolmbl  47089  iinhoiicclem  47101  iunhoiioolem  47103  vonioolem1  47108  vonioolem2  47109  vonicclem1  47111  vonicclem2  47112  decsmf  47195  smflimlem4  47202  smfmullem4  47222  smfco  47230  smfpimcclem  47235  smflimsupmpt  47257  smfliminfmpt  47260  opabresex0d  47733  setsnidel  47837  isupwlkg  48613  isprsd  49430  initc  49566  funcoppc2  49618  swapfval  49737  fucofvalg  49793  prcofvalg  49851  lanfval  50088  ranfval  50089