Theorem elexd 3516

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3496

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-v 3498

This theorem is referenced by:  reuhypd  5322  ideqg  5724  elrnmptg  5833  dmmptd  6495  elfvex  6705  fvmptd3f  6785  fvmptdv2  6788  fmptpr  6936  tpres  6965  ovmpodxf  7302  ovmpodf  7308  offval22  7785  mptsuppd  7855  suppssov1  7864  suppssfv  7868  oeeu  8231  mapsnend  8590  cantnfp1lem2  9144  cantnflem3  9156  oef1o  9163  cnfcomlem  9164  pm54.43lem  9430  ttukeylem3  9935  mptnn0fsupp  13368  mptnn0fsuppr  13370  seqf1olem2  13413  hashbclem  13813  fsumrlim  15168  strfv2d  16531  prdsval  16730  prdssca  16731  imasval  16786  qusval  16817  xpsfrnel  16837  xpsval  16845  cofuval  17154  resfval  17164  funcres2c  17173  setcval  17339  catcval  17358  estrcval  17376  estrres  17391  xpcval  17429  prfval  17451  curfval  17475  uncfval  17486  pospropd  17746  ipodrsima  17777  gsumvalx  17888  prdsmndd  17946  prds0g  17947  prdsgrpd  18211  prdsinvgd  18212  eqgval  18331  prdscmnd  18983  isunit  19409  isirred  19451  issrng  19623  prdslmodd  19743  psrval  20144  mvrfval  20202  opsrval  20257  selvffval  20331  mhpfval  20334  frlmphllem  20926  elfilspd  20949  mamufval  20998  mvmulfval  21153  islocfin  22127  elmptrab2  22438  alexsub  22655  tsmsval2  22740  prdsdsf  22979  prdsxmet  22981  itg2gt0  24363  itgfsum  24429  mtest  24994  mirval  26443  israg  26485  perpln1  26498  perpln2  26499  isperp  26500  midf  26564  ismidb  26566  lmif  26573  islmib  26575  f1otrg  26659  f1otrge  26660  structtocusgr  27230  1loopgrnb0  27286  iswlkg  27397  unidifsnne  30298  funcnvmpt  30414  linds2eq  30943  lindfpropd  30944  dimpropd  31009  ofcfval  31359  sitgval  31592  breprexplema  31903  lpadval  31949  bnj1463  32329  wsuclem  33114  bj-inexeqex  34448  bj-idreseq  34456  bj-idreseqb  34457  bj-ideqg1ALT  34459  bj-imdirval  34474  opelopab3  34994  pren2d  39922  frege81d  40099  frege129d  40115  rfovd  40354  fsovd  40361  fsovrfovd  40362  dssmapfvd  40370  rr-spce  40564  grurankcld  40576  mnurnd  40626  dmmptdf  41495  dmmptdf2  41510  limsupvaluz  41996  limsupequzmpt2  42006  limsupvaluz2  42026  liminfequzmpt2  42079  xlimliminflimsup  42150  rrxsnicc  42592  ioorrnopnlem  42596  ioorrnopnxrlem  42598  subsaliuncl  42648  sge0xaddlem1  42722  sge0xaddlem2  42723  sge0xadd  42724  sge0splitsn  42730  meaiininclem  42775  hoicvrrex  42845  ovn0lem  42854  hoidmvlelem3  42886  ovnhoilem1  42890  hoicoto2  42894  hoidifhspval3  42908  hoiqssbllem1  42911  ovolval4lem1  42938  vonvolmbl  42950  iinhoiicclem  42962  iunhoiioolem  42964  vonioolem1  42969  vonioolem2  42970  vonicclem1  42972  vonicclem2  42973  decsmf  43050  smflimlem4  43057  smfmullem4  43076  smfco  43084  smfpimcclem  43088  smflimsupmpt  43110  smfliminfmpt  43113  opabresex0d  43491  setsnidel  43544  isupwlkg  44019  rngcval  44240  ringcval  44286