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

Theorem elexd 3443
Description: If a class is a member of another class, then it is a set. Deduction associated with elex 3441. (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 3441 . 2 (𝐴𝑉𝐴 ∈ V)
31, 2syl 17 1 (𝜑𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  Vcvv 3423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2717  df-cleq 2731  df-clel 2818  df-v 3425
This theorem is referenced by:  ifexd  4504  reuhypd  5329  ideqg  5738  elrnmptg  5846  dmmptd  6545  elfvex  6772  fvmptd3f  6855  fvmptdv2  6858  tpres  7038  ovmpodxf  7381  ovmpodf  7387  offval22  7878  mptsuppd  7953  suppssov1  7964  suppssfv  7968  ordtypelem9  9172  cantnfp1lem2  9324  cantnflem3  9336  cnfcomlem  9344  ttukeylem3  10155  mptnn0fsupp  13602  mptnn0fsuppr  13604  seqf1olem2  13648  rtrclreclem1  14653  rtrclreclem2  14655  fsumrlim  15408  strfv2d  16785  prdsval  16993  imasval  17049  qusval  17080  xpsfrnel  17100  xpsval  17108  cofuval  17421  resfval  17431  funcres2c  17441  setcval  17616  catcval  17639  estrcval  17664  estrres  17679  xpcval  17717  prfval  17739  curfval  17764  uncfval  17775  isposd  17863  pospropd  17866  ipodrsima  18080  gsumvalx  18181  prdsmndd  18239  prds0g  18240  prdsgrpd  18506  prdsinvgd  18507  eqgval  18626  prdscmnd  19279  isunit  19708  isirred  19750  prdslmodd  20039  frlmphllem  20775  psrval  20906  mvrfval  20977  opsrval  21035  selvffval  21108  mhpfval  21111  mhpmulcl  21121  mamufval  21316  mvmulfval  21471  islocfin  22446  elmptrab2  22757  alexsub  22974  tsmsval2  23059  prdsdsf  23297  prdsxmet  23299  itg2gt0  24690  itgfsum  24756  mtest  25328  mirval  26778  israg  26820  perpln1  26833  perpln2  26834  isperp  26835  midf  26899  ismidb  26901  lmif  26908  islmib  26910  f1otrg  26994  f1otrge  26995  structtocusgr  27566  iswlkg  27733  unidifsnne  30635  iinabrex  30659  funcnvmpt  30756  mgcoval  31015  linds2eq  31321  elrspunidl  31352  rhmpreimacnlem  31580  ofcfval  31810  sitgval  32043  breprexplema  32354  lpadval  32400  bnj1463  32779  fineqvrep  32808  fineqvpow  32809  wsuclem  33590  ssltd  33757  bj-inexeqex  35096  bj-idreseq  35104  bj-idreseqb  35105  bj-ideqg1ALT  35107  bj-imdirvallem  35122  opelopab3  35649  pren2d  40887  frege81d  41080  frege129d  41096  rfovd  41334  fsovd  41341  fsovrfovd  41342  dssmapfvd  41350  rr-spce  41541  mnringvald  41552  grurankcld  41572  mnurnd  41622  dmmptdf  42484  dmmptdf2  42497  limsupequzmpt2  42980  limsupvaluz2  43000  liminfequzmpt2  43053  xlimliminflimsup  43124  rrxsnicc  43562  ioorrnopnlem  43566  ioorrnopnxrlem  43568  subsaliuncl  43618  sge0xaddlem1  43692  sge0xaddlem2  43693  sge0xadd  43694  sge0splitsn  43700  meaiininclem  43745  hoicvrrex  43815  ovn0lem  43824  hoidmvlelem3  43856  ovnhoilem1  43860  hoicoto2  43864  hoidifhspval3  43878  hoiqssbllem1  43881  ovolval4lem1  43908  vonvolmbl  43920  iinhoiicclem  43932  iunhoiioolem  43934  vonioolem1  43939  vonioolem2  43940  vonicclem1  43942  vonicclem2  43943  decsmf  44020  smflimlem4  44027  smfmullem4  44046  smfco  44054  smfpimcclem  44058  smflimsupmpt  44080  smfliminfmpt  44083  opabresex0d  44495  setsnidel  44548  isupwlkg  45018  rngcval  45239  ringcval  45285  isprsd  45968
  Copyright terms: Public domain W3C validator