Theorem elexd 3346

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 3344	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2131  Vcvv 3332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-12 2188  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1627  df-ex 1846  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-v 3334

This theorem is referenced by:  reuhypd  5036  ideqg  5421  elrnmptg  5522  fvmptd3f  6449  pospropd  17327  gsumvalx  17463  isunit  18849  israg  25783  structtocusgr  26544  1loopgrnb0  26600  iswlkg  26711  sitgval  30695  breprexplema  31009  bnj1463  31422  wsuclem  32068  rfovd  38789  fsovd  38796  fsovrfovd  38797  dssmapfvd  38805  projf1o  39877  mapsnend  39882  limsupvaluz  40435  limsupequzmpt2  40445  limsupvaluz2  40465  liminfequzmpt2  40518  rrxsnicc  41015  ioorrnopnlem  41019  ioorrnopnxrlem  41021  subsaliuncl  41071  sge0xaddlem1  41145  sge0xaddlem2  41146  sge0xadd  41147  sge0splitsn  41153  meaiininclem  41198  hoiprodcl2  41267  hoicvrrex  41268  ovn0lem  41277  hoidmvlelem3  41309  ovnhoilem1  41313  hoicoto2  41317  hoidifhspval3  41331  hoiqssbllem1  41334  ovolval4lem1  41361  vonvolmbl  41373  iinhoiicclem  41385  iunhoiioolem  41387  vonioolem1  41392  vonioolem2  41393  vonicclem1  41395  vonicclem2  41396  decsmf  41473  smflimlem4  41480  smfmullem4  41499  smfco  41507  smfpimcclem  41511  smflimsuplem5  41528  smflimsupmpt  41533  smfliminfmpt  41536  opabresex0d  41804  setsnidel  41849  isupwlkg  42220