Theorem elexd 3187

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	⊢ (𝜑 → 𝐴 ∈ 𝑉)

Assertion

Ref	Expression
elexd	⊢ (𝜑 → 𝐴 ∈ V)

Proof of Theorem elexd

Step	Hyp	Ref	Expression
1		elexd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		elex 3185	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 1977  Vcvv 3173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-tru 1478  df-ex 1696  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175

This theorem is referenced by:  reuhypd  4821  ideqg  5195  elrnmptg  5296  fvmptdf  6204  fvmptopab1  6594  gsumvalx  17093  isunit  18480  israg  25392  sitgval  29721  wsuclem  31017  rfovd  37315  fsovd  37322  fsovrfovd  37323  dssmapfvd  37331  projf1o  38381  mapsnend  38386  rrxsnicc  39196  ioorrnopnlem  39200  ioorrnopnxrlem  39202  subsaliuncl  39252  sge0xaddlem1  39326  sge0xaddlem2  39327  sge0xadd  39328  sge0splitsn  39334  meaiuninclem  39373  meaiininclem  39376  hoiprodcl2  39445  hoicvrrex  39446  ovn0lem  39455  hoidmvlelem3  39487  ovnhoilem1  39491  hoicoto2  39495  hoidifhspval3  39509  hoiqssbllem1  39512  ovolval4lem1  39539  ovnovollem2  39547  vonvolmbl  39551  iinhoiicclem  39564  iunhoiioolem  39566  vonioolem1  39571  vonioolem2  39572  vonicclem1  39574  vonicclem2  39575  decsmf  39653  smflimlem4  39660  smfmullem4  39679  smfco  39687  opabresex0d  40330  1loopgrnb0  40717  is1wlkg  40816