Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elexd Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 elexd.1 . 2 (𝜑𝐴𝑉)
2 elex 3344 . 2 (𝐴𝑉𝐴 ∈ V)
31, 2syl 17 1 (𝜑𝐴 ∈ V)
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator