Theorem elexd 3473

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  ifexd  4531  rabexg  5302  reuhypd  5384  ideqg  5831  elrnmptg  5945  dmmptd  6677  elfvex  6913  funcnvmpt  6988  fvmptd3f  7002  fvmptdv2  7005  tpres  7200  ovmpodxf  7563  ovmpodf  7569  mptmpoopabbrd  8080  offval22  8085  mptsuppd  8185  suppssov1  8195  suppssov2  8196  suppssfv  8200  ordtypelem9  9498  cantnfp1lem2  9658  cantnflem3  9670  cnfcomlem  9678  ttukeylem3  10513  mptnn0fsupp  14061  mptnn0fsuppr  14063  seqf1olem2  14106  rtrclreclem1  15130  rtrclreclem2  15132  fsumrlim  15898  strfv2d  17293  prdsval  17540  imasval  17597  qusval  17628  xpsfrnel  17648  xpsval  17656  cofuval  17971  resfval  17981  funcres2c  17992  setcval  18166  catcval  18189  estrcval  18212  estrres  18227  xpcval  18265  prfval  18287  curfval  18311  uncfval  18322  isposd  18410  pospropd  18413  ipodrsima  18629  gsumvalx  18778  prdssgrpd  18835  prdsmndd  18877  prds0g  18878  prdsgrpd  19173  prdsinvgd  19174  eqgval  19302  prdscmnd  19988  isunit  20514  isirred  20560  isrim0  20624  rngcval  20780  ringcval  20809  prdslmodd  21153  frlmphllem  21993  psrval  22130  mvrfval  22195  opsrval  22262  selvffval  22334  mhpfval  22366  mhpmulcl  22377  psdffval  22385  evl1maprhm  22604  mamufval  22614  mvmulfval  22764  islocfin  23743  elmptrab2  24054  alexsub  24271  tsmsval2  24356  prdsdsf  24593  prdsxmet  24595  itg2gt0  25988  itgfsum  26054  mtest  26640  sltsd  28033  seqsp1  28576  mirval  29006  israg  29051  perpln1  29064  perpln2  29065  isperp  29066  tgplnfn  29132  plngval  29134  isplng  29135  midf  29160  ismidb  29162  lmif  29169  islmib  29171  cgrabasimass  29257  brprlng  29295  f1otrg  29327  f1otrge  29328  structtocusgr  29906  iswlkg  30073  unidifsnne  33011  iinabrex  33042  fdifsupp  33157  mgcoval  33426  fxpval  33605  elrgspnlem3  33684  rlocval  33699  subrdom  33725  fldgenval  33753  islbs5  33813  linds2eq  33814  elrspunidl  33856  0mplrim  34024  extvval  34041  splyval  34069  esplyval  34072  resssra  34097  exsslsb  34107  irngval  34195  minplyval  34215  algextdeglem4  34230  constrextdg2lem  34258  constrext2chnlem  34260  rhmpreimacnlem  34394  ofcfval  34608  sitgval  34843  breprexplema  35138  lpadval  35187  bnj1463  35564  fineqvrep  35640  fineqvpow  35641  fineqvnttrclse  35650  wevgblacfn  35708  wsuclem  36402  bj-inexeqex  37906  bj-idreseq  37914  bj-idreseqb  37915  bj-ideqg1ALT  37917  bj-imdirvallem  37932  opelopab3  38468  aks6d1c6lem2  43037  aks5lem2  43053  onsupex3  44075  pren2d  44396  frege81d  44587  frege129d  44603  rfovd  44841  fsovd  44848  fsovrfovd  44849  dssmapfvd  44857  rr-spce  45042  mnringvald  45051  grurankcld  45071  mnurnd  45107  dmmptdff  46053  dmmptdf2  46062  limsupequzmpt2  46546  liminfequzmpt2  46619  xlimliminflimsup  46690  rrxsnicc  47128  ioorrnopnlem  47132  ioorrnopnxrlem  47134  subsaliuncl  47186  sge0xaddlem1  47261  sge0xaddlem2  47262  sge0xadd  47263  sge0splitsn  47269  meaiininclem  47314  hoicvrrex  47384  ovn0lem  47393  hoidmvlelem3  47425  ovnhoilem1  47429  hoicoto2  47433  hoidifhspval3  47447  hoiqssbllem1  47450  ovolval4lem1  47477  vonvolmbl  47489  iinhoiicclem  47501  iunhoiioolem  47503  vonioolem1  47508  vonioolem2  47509  vonicclem1  47511  vonicclem2  47512  decsmf  47595  smflimlem4  47602  smfmullem4  47622  smfco  47630  smfpimcclem  47635  smflimsupmpt  47657  smfliminfmpt  47660  opabresex0d  48173  setsnidel  48277  isupwlkg  49053  isprsd  49881  initc  50017  funcoppc2  50069  swapfval  50188  fucofvalg  50244  prcofvalg  50302  lanfval  50539  ranfval  50540