Theorem elexd 3214

Description: If a class is a member of another class, it is a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.)

Hypothesis

Ref	Expression
elexd.1	|- ( ph -> A e. V )

Assertion

Ref	Expression
elexd	|- ( ph -> A e. _V )

Proof of Theorem elexd

Step	Hyp	Ref	Expression
1		elexd.1	. 2 |- ( ph -> A e. V )
2		elex 3212	. 2 |- ( A e. V -> A e. _V )
3	1, 2	syl 17	1 |- ( ph -> A e. _V )

Syntax hints:   -> wi 4   e. wcel 1990   _Vcvv 3200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1486  df-ex 1705  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202

This theorem is referenced by:  reuhypd  4895  ideqg  5273  elrnmptg  5375  fvmptd3f  6295  pospropd  17134  gsumvalx  17270  isunit  18657  israg  25592  structtocusgr  26342  1loopgrnb0  26398  iswlkg  26509  sitgval  30394  breprexplema  30708  bnj1463  31123  wsuclem  31773  rfovd  38295  fsovd  38302  fsovrfovd  38303  dssmapfvd  38311  projf1o  39386  mapsnend  39391  limsupvaluz  39940  limsupequzmpt2  39950  limsupvaluz2  39970  liminfequzmpt2  40023  rrxsnicc  40520  ioorrnopnlem  40524  ioorrnopnxrlem  40526  subsaliuncl  40576  sge0xaddlem1  40650  sge0xaddlem2  40651  sge0xadd  40652  sge0splitsn  40658  meaiininclem  40700  hoiprodcl2  40769  hoicvrrex  40770  ovn0lem  40779  hoidmvlelem3  40811  ovnhoilem1  40815  hoicoto2  40819  hoidifhspval3  40833  hoiqssbllem1  40836  ovolval4lem1  40863  vonvolmbl  40875  iinhoiicclem  40887  iunhoiioolem  40889  vonioolem1  40894  vonioolem2  40895  vonicclem1  40897  vonicclem2  40898  decsmf  40975  smflimlem4  40982  smfmullem4  41001  smfco  41009  smfpimcclem  41013  smflimsuplem5  41030  smflimsupmpt  41035  smfliminfmpt  41038  opabresex0d  41304  setsnidel  41347  isupwlkg  41718