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

Theorem elexd 3468
Description: If a class is a member of another class, then it is a set. Deduction associated with elex 3466. (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 3466 . 2 (𝐴𝑉𝐴 ∈ V)
31, 2syl 17 1 (𝜑𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  Vcvv 3448
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450
This theorem is referenced by:  ifexd  4539  reuhypd  5379  ideqg  5812  elrnmptg  5919  dmmptd  6651  elfvex  6885  fvmptd3f  6968  fvmptdv2  6971  tpres  7155  ovmpodxf  7510  ovmpodf  7516  mptmpoopabbrd  8018  offval22  8025  mptsuppd  8123  suppssov1  8134  suppssfv  8138  ordtypelem9  9469  cantnfp1lem2  9622  cantnflem3  9634  cnfcomlem  9642  ttukeylem3  10454  mptnn0fsupp  13909  mptnn0fsuppr  13911  seqf1olem2  13955  rtrclreclem1  14949  rtrclreclem2  14951  fsumrlim  15703  strfv2d  17081  prdsval  17344  imasval  17400  qusval  17431  xpsfrnel  17451  xpsval  17459  cofuval  17775  resfval  17785  funcres2c  17795  setcval  17970  catcval  17993  estrcval  18018  estrres  18034  xpcval  18072  prfval  18094  curfval  18119  uncfval  18130  isposd  18219  pospropd  18223  ipodrsima  18437  gsumvalx  18538  prdsmndd  18596  prds0g  18597  prdsgrpd  18864  prdsinvgd  18865  eqgval  18986  prdscmnd  19646  isunit  20093  isirred  20137  isrim0  20165  prdslmodd  20446  frlmphllem  21202  psrval  21333  mvrfval  21405  opsrval  21463  selvffval  21542  mhpfval  21545  mhpmulcl  21555  mamufval  21750  mvmulfval  21907  islocfin  22884  elmptrab2  23195  alexsub  23412  tsmsval2  23497  prdsdsf  23736  prdsxmet  23738  itg2gt0  25141  itgfsum  25207  mtest  25779  ssltd  27153  mirval  27639  israg  27681  perpln1  27694  perpln2  27695  isperp  27696  midf  27760  ismidb  27762  lmif  27769  islmib  27771  f1otrg  27855  f1otrge  27856  structtocusgr  28436  iswlkg  28603  unidifsnne  31505  iinabrex  31529  funcnvmpt  31625  mgcoval  31888  fldgenval  32121  linds2eq  32208  elrspunidl  32243  irngval  32399  minplyval  32412  rhmpreimacnlem  32505  ofcfval  32737  sitgval  32972  breprexplema  33283  lpadval  33329  bnj1463  33707  fineqvrep  33736  fineqvpow  33737  wsuclem  34439  bj-inexeqex  35654  bj-idreseq  35662  bj-idreseqb  35663  bj-ideqg1ALT  35665  bj-imdirvallem  35680  opelopab3  36205  onsupex3  41597  pren2d  41902  frege81d  42093  frege129d  42109  rfovd  42347  fsovd  42354  fsovrfovd  42355  dssmapfvd  42363  rr-spce  42551  mnringvald  42562  grurankcld  42587  mnurnd  42637  dmmptdff  43518  dmmptdf2  43532  limsupequzmpt2  44033  limsupvaluz2  44053  liminfequzmpt2  44106  xlimliminflimsup  44177  rrxsnicc  44615  ioorrnopnlem  44619  ioorrnopnxrlem  44621  subsaliuncl  44673  sge0xaddlem1  44748  sge0xaddlem2  44749  sge0xadd  44750  sge0splitsn  44756  meaiininclem  44801  hoicvrrex  44871  ovn0lem  44880  hoidmvlelem3  44912  ovnhoilem1  44916  hoicoto2  44920  hoidifhspval3  44934  hoiqssbllem1  44937  ovolval4lem1  44964  vonvolmbl  44976  iinhoiicclem  44988  iunhoiioolem  44990  vonioolem1  44995  vonioolem2  44996  vonicclem1  44998  vonicclem2  44999  decsmf  45082  smflimlem4  45089  smfmullem4  45109  smfco  45117  smfpimcclem  45122  smflimsupmpt  45144  smfliminfmpt  45147  opabresex0d  45591  setsnidel  45643  isupwlkg  46113  rngcval  46334  ringcval  46380  isprsd  47062
  Copyright terms: Public domain W3C validator