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

Theorem elexd 3491
Description: If a class is a member of another class, then it is a set. Deduction associated with elex 3489. (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 3489 . 2 (𝐴𝑉𝐴 ∈ V)
31, 2syl 17 1 (𝜑𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  Vcvv 3471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-v 3473
This theorem is referenced by:  reuhypd  5293  ideqg  5695  elrnmptg  5804  dmmptd  6466  elfvex  6676  fvmptd3f  6756  fvmptdv2  6759  fmptpr  6907  tpres  6936  ovmpodxf  7274  ovmpodf  7280  offval22  7758  mptsuppd  7828  suppssov1  7837  suppssfv  7841  oeeu  8204  mapsnend  8563  cantnfp1lem2  9118  cantnflem3  9130  oef1o  9137  cnfcomlem  9138  pm54.43lem  9405  ttukeylem3  9910  mptnn0fsupp  13348  mptnn0fsuppr  13350  seqf1olem2  13394  hashbclem  13794  fsumrlim  15145  strfv2d  16508  prdsval  16707  prdssca  16708  imasval  16763  qusval  16794  xpsfrnel  16814  xpsval  16822  cofuval  17131  resfval  17141  funcres2c  17150  setcval  17316  catcval  17335  estrcval  17353  estrres  17368  xpcval  17406  prfval  17428  curfval  17452  uncfval  17463  isposd  17544  pospropd  17723  ipodrsima  17754  gsumvalx  17865  prdsmndd  17923  prds0g  17924  prdsgrpd  18188  prdsinvgd  18189  eqgval  18308  prdscmnd  18960  isunit  19386  isirred  19428  issrng  19597  prdslmodd  19717  psrval  20118  mvrfval  20176  opsrval  20231  selvffval  20305  mhpfval  20308  frlmphllem  20900  mamufval  20972  mvmulfval  21127  islocfin  22101  elmptrab2  22412  alexsub  22629  tsmsval2  22714  prdsdsf  22953  prdsxmet  22955  itg2gt0  24343  itgfsum  24409  mtest  24978  mirval  26428  israg  26470  perpln1  26483  perpln2  26484  isperp  26485  midf  26549  ismidb  26551  lmif  26558  islmib  26560  f1otrg  26644  f1otrge  26645  structtocusgr  27215  1loopgrnb0  27271  iswlkg  27382  unidifsnne  30283  funcnvmpt  30399  mgcoval  30655  linds2eq  30950  ofcfval  31365  sitgval  31598  breprexplema  31909  lpadval  31955  bnj1463  32335  wsuclem  33120  bj-inexeqex  34464  bj-idreseq  34472  bj-idreseqb  34473  bj-ideqg1ALT  34475  bj-imdirval  34490  opelopab3  35037  pren2d  40062  frege81d  40255  frege129d  40271  rfovd  40510  fsovd  40517  fsovrfovd  40518  dssmapfvd  40526  rr-spce  40720  mnringvald  40732  grurankcld  40752  mnurnd  40802  dmmptdf  41670  dmmptdf2  41685  limsupvaluz  42169  limsupequzmpt2  42179  limsupvaluz2  42199  liminfequzmpt2  42252  xlimliminflimsup  42323  rrxsnicc  42761  ioorrnopnlem  42765  ioorrnopnxrlem  42767  subsaliuncl  42817  sge0xaddlem1  42891  sge0xaddlem2  42892  sge0xadd  42893  sge0splitsn  42899  meaiininclem  42944  hoicvrrex  43014  ovn0lem  43023  hoidmvlelem3  43055  ovnhoilem1  43059  hoicoto2  43063  hoidifhspval3  43077  hoiqssbllem1  43080  ovolval4lem1  43107  vonvolmbl  43119  iinhoiicclem  43131  iunhoiioolem  43133  vonioolem1  43138  vonioolem2  43139  vonicclem1  43141  vonicclem2  43142  decsmf  43219  smflimlem4  43226  smfmullem4  43245  smfco  43253  smfpimcclem  43257  smflimsupmpt  43279  smfliminfmpt  43282  opabresex0d  43660  setsnidel  43713  isupwlkg  44184  rngcval  44405  ringcval  44451
  Copyright terms: Public domain W3C validator