Theorem elexd 3512

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490

This theorem is referenced by:  ifexd  4596  rabexg  5355  reuhypd  5437  ideqg  5876  elrnmptg  5984  dmmptd  6725  elfvex  6958  fvmptd3f  7044  fvmptdv2  7047  tpres  7238  ovmpodxf  7600  ovmpodf  7606  mptmpoopabbrd  8121  mptmpoopabbrdOLD  8122  offval22  8129  mptsuppd  8228  suppssov1  8238  suppssov2  8239  suppssfv  8243  ordtypelem9  9595  cantnfp1lem2  9748  cantnflem3  9760  cnfcomlem  9768  ttukeylem3  10580  mptnn0fsupp  14048  mptnn0fsuppr  14050  seqf1olem2  14093  rtrclreclem1  15106  rtrclreclem2  15108  fsumrlim  15859  strfv2d  17249  prdsval  17515  imasval  17571  qusval  17602  xpsfrnel  17622  xpsval  17630  cofuval  17946  resfval  17956  funcres2c  17968  setcval  18144  catcval  18167  estrcval  18192  estrres  18208  xpcval  18246  prfval  18268  curfval  18293  uncfval  18304  isposd  18393  pospropd  18397  ipodrsima  18611  gsumvalx  18714  prdssgrpd  18771  prdsmndd  18805  prds0g  18806  prdsgrpd  19090  prdsinvgd  19091  eqgval  19217  prdscmnd  19903  isunit  20399  isirred  20445  isrim0  20509  rngcval  20640  ringcval  20669  prdslmodd  20990  frlmphllem  21823  psrval  21958  mvrfval  22024  opsrval  22087  selvffval  22160  mhpfval  22165  mhpmulcl  22176  psdffval  22184  evl1maprhm  22404  mamufval  22417  mvmulfval  22569  islocfin  23546  elmptrab2  23857  alexsub  24074  tsmsval2  24159  prdsdsf  24398  prdsxmet  24400  itg2gt0  25815  itgfsum  25882  mtest  26465  ssltd  27854  seqsp1  28335  mirval  28681  israg  28723  perpln1  28736  perpln2  28737  isperp  28738  midf  28802  ismidb  28804  lmif  28811  islmib  28813  f1otrg  28897  f1otrge  28898  structtocusgr  29481  iswlkg  29649  unidifsnne  32564  iinabrex  32591  funcnvmpt  32685  mgcoval  32959  rlocval  33231  subrdom  33254  fldgenval  33279  islbs5  33373  linds2eq  33374  elrspunidl  33421  resssra  33602  irngval  33685  minplyval  33698  algextdeglem4  33711  rhmpreimacnlem  33830  ofcfval  34062  sitgval  34297  breprexplema  34607  lpadval  34653  bnj1463  35031  fineqvrep  35071  fineqvpow  35072  wevgblacfn  35076  wsuclem  35789  bj-inexeqex  37120  bj-idreseq  37128  bj-idreseqb  37129  bj-ideqg1ALT  37131  bj-imdirvallem  37146  opelopab3  37678  aks6d1c6lem2  42128  aks5lem2  42144  onsupex3  43195  pren2d  43518  frege81d  43709  frege129d  43725  rfovd  43963  fsovd  43970  fsovrfovd  43971  dssmapfvd  43979  rr-spce  44166  mnringvald  44177  grurankcld  44202  mnurnd  44252  dmmptdff  45130  dmmptdf2  45140  limsupequzmpt2  45639  limsupvaluz2  45659  liminfequzmpt2  45712  xlimliminflimsup  45783  rrxsnicc  46221  ioorrnopnlem  46225  ioorrnopnxrlem  46227  subsaliuncl  46279  sge0xaddlem1  46354  sge0xaddlem2  46355  sge0xadd  46356  sge0splitsn  46362  meaiininclem  46407  hoicvrrex  46477  ovn0lem  46486  hoidmvlelem3  46518  ovnhoilem1  46522  hoicoto2  46526  hoidifhspval3  46540  hoiqssbllem1  46543  ovolval4lem1  46570  vonvolmbl  46582  iinhoiicclem  46594  iunhoiioolem  46596  vonioolem1  46601  vonioolem2  46602  vonicclem1  46604  vonicclem2  46605  decsmf  46688  smflimlem4  46695  smfmullem4  46715  smfco  46723  smfpimcclem  46728  smflimsupmpt  46750  smfliminfmpt  46753  opabresex0d  47200  setsnidel  47251  isupwlkg  47860  isprsd  48635