Theorem elexd 3430

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

Syntax hints:   → wi 4   ∈ wcel 2166  Vcvv 3413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-12 2222  ax-ext 2802

This theorem depends on definitions:  df-bi 199  df-an 387  df-tru 1662  df-ex 1881  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-v 3415

This theorem is referenced by:  reuhypd  5122  ideqg  5505  elrnmptg  5607  fvmptd3f  6541  mapsnend  8300  strfv2d  16267  estrres  17131  pospropd  17486  gsumvalx  17622  isunit  19010  israg  26008  structtocusgr  26743  1loopgrnb0  26799  iswlkg  26910  funcnvmpt  30015  sitgval  30938  breprexplema  31256  bnj1463  31668  wsuclem  32308  rfovd  39134  fsovd  39141  fsovrfovd  39142  dssmapfvd  39150  limsupvaluz  40734  limsupequzmpt2  40744  limsupvaluz2  40764  liminfequzmpt2  40817  rrxsnicc  41310  ioorrnopnlem  41314  ioorrnopnxrlem  41316  subsaliuncl  41366  sge0xaddlem1  41440  sge0xaddlem2  41441  sge0xadd  41442  sge0splitsn  41448  meaiininclem  41493  hoicvrrex  41563  ovn0lem  41572  hoidmvlelem3  41604  ovnhoilem1  41608  hoicoto2  41612  hoidifhspval3  41626  hoiqssbllem1  41629  ovolval4lem1  41656  vonvolmbl  41668  iinhoiicclem  41680  iunhoiioolem  41682  vonioolem1  41687  vonioolem2  41688  vonicclem1  41690  vonicclem2  41691  decsmf  41768  smflimlem4  41775  smfmullem4  41794  smfco  41802  smfpimcclem  41806  smflimsupmpt  41828  smfliminfmpt  41831  opabresex0d  42187  setsnidel  42234  isupwlkg  42564