Theorem elexd 3477

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  Vcvv 3454

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456

This theorem is used by:  ifexd  4534  rabexg  5306  reuhypd  5388  ideqg  5839  elrnmptg  5955  dmmptd  6714  elfvex  6951  funcnvmpt  7026  fvmptd3f  7040  fvmptdv2  7043  tpres  7238  ovmpodxf  7602  ovmpodf  7608  mpt3fvd  7720  mptmpoopabbrd  8129  offval22  8134  mptsuppd  8242  suppssov1  8252  suppssov2  8253  suppssfv  8257  ordtypelem9  9557  cantnfp1lem2  9717  cantnflem3  9729  cnfcomlem  9737  ttukeylem3  10628  mptnn0fsupp  14180  mptnn0fsuppr  14182  seqf1olem2  14225  rtrclreclem1  15253  rtrclreclem2  15255  fsumrlim  16022  strfv2d  17423  prdsval  17676  imasval  17733  qusval  17764  xpsfrnel  17784  xpsval  17792  cofuval  18107  resfval  18117  funcres2c  18128  setcval  18302  catcval  18325  estrcval  18348  estrres  18363  xpcval  18401  prfval  18423  curfval  18447  uncfval  18458  isposd  18546  pospropd  18549  ipodrsima  18765  gsumvalx  18915  prdssgrpd  18972  prdsmndd  19014  prds0g  19015  prdsgrpd  19310  prdsinvgd  19311  eqgval  19439  prdscmnd  20126  isunit  20654  isirred  20700  isrim0  20764  rngcval  20921  ringcval  20950  prdslmodd  21295  frlmphllem  22141  psrval  22278  mvrfval  22343  opsrval  22410  selvffval  22482  mhpfval  22514  mhpmulcl  22525  psdffval  22533  evl1maprhm  22752  mamufval  22762  mvmulfval  22912  islocfin  23891  elmptrab2  24202  alexsub  24419  tsmsval2  24504  prdsdsf  24741  prdsxmet  24743  itg2gt0  26136  itgfsum  26202  mtest  26788  sltsd  28211  seqsp1  28754  mirval  29184  israg  29229  perpln1  29242  perpln2  29243  isperp  29244  tgplnfn  29310  plngval  29312  isplng  29313  midf  29338  ismidb  29340  lmif  29347  islmib  29349  cgrabasimass  29435  brprlng  29473  f1otrg  29505  f1otrge  29506  structtocusgr  30084  iswlkg  30251  tgextalem1inag  33127  unidifsnne  33230  iinabrex  33261  fdifsupp  33375  mgcoval  33646  fxpval  33825  elrgspnlem3  33904  rlocval  33919  subrdom  33945  fldgenval  33978  islbs5  34039  linds2eq  34040  0mplrim  34257  extvval  34274  splyval  34302  esplyval  34305  resssra  34330  exsslsb  34340  irngval  34428  minplyval  34448  algextdeglem4  34463  constrextdg2lem  34491  constrext2chnlem  34493  rhmpreimacnlem  34627  ofcfval  34841  sitgval  35075  breprexplema  35370  lpadval  35419  bnj1463  35796  mpofvd  35838  fineqvrep  35923  fineqvpow  35924  fineqvnttrclse  35933  gdlop1fv  36004  gdlop2fv  36005  gdlop3fv  36006  gdlop4fv  36007  gdlop5fv  36008  gdlop6fv  36009  gdlop7fv  36010  gdlop8fv  36011  gdlopcfv1  36013  gdlopcfv2  36014  gdlopcfv3  36015  gdlopcfv4  36016  gdlopcfv5  36017  gdlopcfv6  36018  gdlopcfv7  36019  gdlopcfv8  36020  wevgblacfn  36080  wsuclem  36802  bj-inexeqex  38343  bj-idreseq  38351  bj-idreseqb  38352  bj-ideqg1ALT  38354  bj-imdirvallem  38369  nlpfvineqsn  38600  pibt2  38608  opelopab3  38920  aks6d1c6lem2  43487  aks5lem2  43503  onsupex3  44497  pren2d  44818  frege81d  45008  frege129d  45024  rfovd  45262  fsovd  45269  fsovrfovd  45270  dssmapfvd  45278  rr-spce  45463  mnringvald  45472  grurankcld  45492  mnurnd  45528  dmmptdff  46509  dmmptdf2  46518  limsupequzmpt2  47001  liminfequzmpt2  47074  xlimliminflimsup  47145  rrxsnicc  47583  ioorrnopnlem  47587  ioorrnopnxrlem  47589  subsaliuncl  47641  sge0xaddlem1  47716  sge0xaddlem2  47717  sge0xadd  47718  sge0splitsn  47724  meaiininclem  47769  hoicvrrex  47839  ovn0lem  47848  hoidmvlelem3  47880  ovnhoilem1  47884  hoicoto2  47888  hoidifhspval3  47902  hoiqssbllem1  47905  ovolval4lem1  47932  vonvolmbl  47944  iinhoiicclem  47956  iunhoiioolem  47958  vonioolem1  47963  vonioolem2  47964  vonicclem1  47966  vonicclem2  47967  decsmf  48050  smflimlem4  48057  smfmullem4  48077  smfco  48085  smfpimcclem  48090  smflimsupmpt  48112  smfliminfmpt  48115  opabresex0d  48628  setsnidel  48732  isupwlkg  49508  elovmpoeq  50311  isprsd  50400  ixpovf  50528  initc  50537  funcoppc2  50590  swapfval  50715  fucofvalg  50771  prcofvalg  50842  lanfval  51127  ranfval  51128