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 2144  Vcvv 3450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  ifexd  4530  rabexg  5298  reuhypd  5380  ideqg  5829  elrnmptg  5943  dmmptd  6687  elfvex  6923  funcnvmpt  6998  fvmptd3f  7012  fvmptdv2  7015  tpres  7209  ovmpodxf  7572  ovmpodf  7578  mpt3fvd  7690  mptmpoopabbrd  8096  offval22  8101  mptsuppd  8209  suppssov1  8219  suppssov2  8220  suppssfv  8224  ordtypelem9  9525  cantnfp1lem2  9685  cantnflem3  9697  cnfcomlem  9705  ttukeylem3  10594  mptnn0fsupp  14145  mptnn0fsuppr  14147  seqf1olem2  14190  rtrclreclem1  15217  rtrclreclem2  15219  fsumrlim  15985  strfv2d  17386  prdsval  17633  imasval  17690  qusval  17721  xpsfrnel  17741  xpsval  17749  cofuval  18064  resfval  18074  funcres2c  18085  setcval  18259  catcval  18282  estrcval  18305  estrres  18320  xpcval  18358  prfval  18380  curfval  18404  uncfval  18415  isposd  18503  pospropd  18506  ipodrsima  18722  gsumvalx  18872  prdssgrpd  18929  prdsmndd  18971  prds0g  18972  prdsgrpd  19267  prdsinvgd  19268  eqgval  19396  prdscmnd  20082  isunit  20610  isirred  20656  isrim0  20720  rngcval  20877  ringcval  20906  prdslmodd  21251  frlmphllem  22093  psrval  22230  mvrfval  22295  opsrval  22362  selvffval  22434  mhpfval  22466  mhpmulcl  22477  psdffval  22485  evl1maprhm  22704  mamufval  22714  mvmulfval  22864  islocfin  23843  elmptrab2  24154  alexsub  24371  tsmsval2  24456  prdsdsf  24693  prdsxmet  24695  itg2gt0  26088  itgfsum  26154  mtest  26738  sltsd  28161  seqsp1  28704  mirval  29134  israg  29179  perpln1  29192  perpln2  29193  isperp  29194  tgplnfn  29260  plngval  29262  isplng  29263  midf  29288  ismidb  29290  lmif  29297  islmib  29299  cgrabasimass  29385  brprlng  29423  f1otrg  29455  f1otrge  29456  structtocusgr  30034  iswlkg  30201  tgextalem1inag  33077  unidifsnne  33181  iinabrex  33212  fdifsupp  33327  mgcoval  33595  fxpval  33774  elrgspnlem3  33853  rlocval  33868  subrdom  33894  fldgenval  33922  islbs5  33983  linds2eq  33984  0mplrim  34194  extvval  34211  splyval  34239  esplyval  34242  resssra  34267  exsslsb  34277  irngval  34365  minplyval  34385  algextdeglem4  34400  constrextdg2lem  34428  constrext2chnlem  34430  rhmpreimacnlem  34564  ofcfval  34778  sitgval  35012  breprexplema  35307  lpadval  35356  bnj1463  35733  fineqvrep  35840  fineqvpow  35841  fineqvnttrclse  35850  wevgblacfn  35960  wsuclem  36681  bj-inexeqex  38182  bj-idreseq  38190  bj-idreseqb  38191  bj-ideqg1ALT  38193  bj-imdirvallem  38208  nlpfvineqsn  38439  pibt2  38447  opelopab3  38759  aks6d1c6lem2  43328  aks5lem2  43344  onsupex3  44343  pren2d  44664  frege81d  44854  frege129d  44870  rfovd  45108  fsovd  45115  fsovrfovd  45116  dssmapfvd  45124  rr-spce  45309  mnringvald  45318  grurankcld  45338  mnurnd  45374  dmmptdff  46343  dmmptdf2  46352  limsupequzmpt2  46835  liminfequzmpt2  46908  xlimliminflimsup  46979  rrxsnicc  47417  ioorrnopnlem  47421  ioorrnopnxrlem  47423  subsaliuncl  47475  sge0xaddlem1  47550  sge0xaddlem2  47551  sge0xadd  47552  sge0splitsn  47558  meaiininclem  47603  hoicvrrex  47673  ovn0lem  47682  hoidmvlelem3  47714  ovnhoilem1  47718  hoicoto2  47722  hoidifhspval3  47736  hoiqssbllem1  47739  ovolval4lem1  47766  vonvolmbl  47778  iinhoiicclem  47790  iunhoiioolem  47792  vonioolem1  47797  vonioolem2  47798  vonicclem1  47800  vonicclem2  47801  decsmf  47884  smflimlem4  47891  smfmullem4  47911  smfco  47919  smfpimcclem  47924  smflimsupmpt  47946  smfliminfmpt  47949  opabresex0d  48462  setsnidel  48566  isupwlkg  49342  elovmpoeq  50087  isprsd  50176  ixpovf  50304  initc  50313  funcoppc2  50366  swapfval  50491  fucofvalg  50547  prcofvalg  50618  lanfval  50903  ranfval  50904