Theorem elexd 3514

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3494

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 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-v 3496

This theorem is referenced by:  reuhypd  5320  ideqg  5722  elrnmptg  5831  dmmptd  6493  elfvex  6703  fvmptd3f  6783  fvmptdv2  6786  fmptpr  6934  tpres  6963  ovmpodxf  7300  ovmpodf  7306  offval22  7783  mptsuppd  7853  suppssov1  7862  suppssfv  7866  oeeu  8229  mapsnend  8588  cantnfp1lem2  9142  cantnflem3  9154  oef1o  9161  cnfcomlem  9162  pm54.43lem  9428  ttukeylem3  9933  mptnn0fsupp  13366  mptnn0fsuppr  13368  seqf1olem2  13411  hashbclem  13811  fsumrlim  15166  strfv2d  16529  prdsval  16728  prdssca  16729  imasval  16784  qusval  16815  xpsfrnel  16835  xpsval  16843  cofuval  17152  resfval  17162  funcres2c  17171  setcval  17337  catcval  17356  estrcval  17374  estrres  17389  xpcval  17427  prfval  17449  curfval  17473  uncfval  17484  pospropd  17744  ipodrsima  17775  gsumvalx  17886  prdsmndd  17944  prds0g  17945  prdsgrpd  18209  prdsinvgd  18210  eqgval  18329  prdscmnd  18981  isunit  19407  isirred  19449  issrng  19621  prdslmodd  19741  psrval  20142  mvrfval  20200  opsrval  20255  selvffval  20329  mhpfval  20332  frlmphllem  20924  elfilspd  20947  mamufval  20996  mvmulfval  21151  islocfin  22125  elmptrab2  22436  alexsub  22653  tsmsval2  22738  prdsdsf  22977  prdsxmet  22979  itg2gt0  24361  itgfsum  24427  mtest  24992  mirval  26441  israg  26483  perpln1  26496  perpln2  26497  isperp  26498  midf  26562  ismidb  26564  lmif  26571  islmib  26573  f1otrg  26657  f1otrge  26658  structtocusgr  27228  1loopgrnb0  27284  iswlkg  27395  unidifsnne  30296  funcnvmpt  30412  linds2eq  30941  lindfpropd  30942  dimpropd  31007  ofcfval  31357  sitgval  31590  breprexplema  31901  lpadval  31947  bnj1463  32327  wsuclem  33112  bj-inexeqex  34449  bj-idreseq  34457  bj-idreseqb  34458  bj-ideqg1ALT  34460  bj-imdirval  34475  opelopab3  35007  pren2d  39935  frege81d  40112  frege129d  40128  rfovd  40367  fsovd  40374  fsovrfovd  40375  dssmapfvd  40383  rr-spce  40577  grurankcld  40589  mnurnd  40639  dmmptdf  41508  dmmptdf2  41523  limsupvaluz  42009  limsupequzmpt2  42019  limsupvaluz2  42039  liminfequzmpt2  42092  xlimliminflimsup  42163  rrxsnicc  42605  ioorrnopnlem  42609  ioorrnopnxrlem  42611  subsaliuncl  42661  sge0xaddlem1  42735  sge0xaddlem2  42736  sge0xadd  42737  sge0splitsn  42743  meaiininclem  42788  hoicvrrex  42858  ovn0lem  42867  hoidmvlelem3  42899  ovnhoilem1  42903  hoicoto2  42907  hoidifhspval3  42921  hoiqssbllem1  42924  ovolval4lem1  42951  vonvolmbl  42963  iinhoiicclem  42975  iunhoiioolem  42977  vonioolem1  42982  vonioolem2  42983  vonicclem1  42985  vonicclem2  42986  decsmf  43063  smflimlem4  43070  smfmullem4  43089  smfco  43097  smfpimcclem  43101  smflimsupmpt  43123  smfliminfmpt  43126  opabresex0d  43504  setsnidel  43557  isupwlkg  44032  rngcval  44253  ringcval  44299