Theorem elexd 3454

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

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433

This theorem is referenced by:  ifexd  4503  rabexg  5265  reuhypd  5348  ideqg  5793  elrnmptg  5903  dmmptd  6630  elfvex  6862  funcnvmpt  6937  fvmptd3f  6951  fvmptdv2  6954  tpres  7145  ovmpodxf  7506  ovmpodf  7512  mptmpoopabbrd  8022  offval22  8027  mptsuppd  8127  suppssov1  8137  suppssov2  8138  suppssfv  8142  ordtypelem9  9431  cantnfp1lem2  9591  cantnflem3  9603  cnfcomlem  9611  ttukeylem3  10424  mptnn0fsupp  13950  mptnn0fsuppr  13952  seqf1olem2  13995  rtrclreclem1  15010  rtrclreclem2  15012  fsumrlim  15765  strfv2d  17162  prdsval  17409  imasval  17466  qusval  17497  xpsfrnel  17517  xpsval  17525  cofuval  17840  resfval  17850  funcres2c  17861  setcval  18035  catcval  18058  estrcval  18081  estrres  18096  xpcval  18134  prfval  18156  curfval  18180  uncfval  18191  isposd  18279  pospropd  18282  ipodrsima  18498  gsumvalx  18635  prdssgrpd  18692  prdsmndd  18729  prds0g  18730  prdsgrpd  19017  prdsinvgd  19018  eqgval  19143  prdscmnd  19827  isunit  20344  isirred  20390  isrim0  20453  rngcval  20590  ringcval  20619  prdslmodd  20959  frlmphllem  21755  psrval  21890  mvrfval  21955  opsrval  22022  selvffval  22094  mhpfval  22126  mhpmulcl  22137  psdffval  22145  evl1maprhm  22365  mamufval  22375  mvmulfval  22525  islocfin  23500  elmptrab2  23811  alexsub  24028  tsmsval2  24113  prdsdsf  24350  prdsxmet  24352  itg2gt0  25745  itgfsum  25812  mtest  26387  sltsd  27778  seqsp1  28321  mirval  28741  israg  28783  perpln1  28796  perpln2  28797  isperp  28798  midf  28862  ismidb  28864  lmif  28871  islmib  28873  f1otrg  28957  f1otrge  28958  structtocusgr  29533  iswlkg  29700  unidifsnne  32624  iinabrex  32658  fdifsupp  32777  mgcoval  33065  fxpval  33246  elrgspnlem3  33325  rlocval  33340  subrdom  33366  fldgenval  33396  islbs5  33463  linds2eq  33464  elrspunidl  33511  0mplrim  33698  extvval  33715  splyval  33743  esplyval  33746  resssra  33771  exsslsb  33781  irngval  33869  minplyval  33889  algextdeglem4  33904  constrextdg2lem  33932  constrext2chnlem  33934  rhmpreimacnlem  34068  ofcfval  34282  sitgval  34516  breprexplema  34814  lpadval  34860  bnj1463  35237  fineqvrep  35295  fineqvpow  35296  fineqvnttrclse  35305  wevgblacfn  35337  wsuclem  36051  bj-inexeqex  37514  bj-idreseq  37522  bj-idreseqb  37523  bj-ideqg1ALT  37525  bj-imdirvallem  37540  opelopab3  38085  aks6d1c6lem2  42656  aks5lem2  42672  onsupex3  43679  pren2d  44000  frege81d  44191  frege129d  44207  rfovd  44445  fsovd  44452  fsovrfovd  44453  dssmapfvd  44461  rr-spce  44648  mnringvald  44657  grurankcld  44677  mnurnd  44727  dmmptdff  45668  dmmptdf2  45677  limsupequzmpt2  46161  liminfequzmpt2  46234  xlimliminflimsup  46305  rrxsnicc  46743  ioorrnopnlem  46747  ioorrnopnxrlem  46749  subsaliuncl  46801  sge0xaddlem1  46876  sge0xaddlem2  46877  sge0xadd  46878  sge0splitsn  46884  meaiininclem  46929  hoicvrrex  46999  ovn0lem  47008  hoidmvlelem3  47040  ovnhoilem1  47044  hoicoto2  47048  hoidifhspval3  47062  hoiqssbllem1  47065  ovolval4lem1  47092  vonvolmbl  47104  iinhoiicclem  47116  iunhoiioolem  47118  vonioolem1  47123  vonioolem2  47124  vonicclem1  47126  vonicclem2  47127  decsmf  47210  smflimlem4  47217  smfmullem4  47237  smfco  47245  smfpimcclem  47250  smflimsupmpt  47272  smfliminfmpt  47275  opabresex0d  47748  setsnidel  47852  isupwlkg  48628  isprsd  49445  initc  49581  funcoppc2  49633  swapfval  49752  fucofvalg  49808  prcofvalg  49866  lanfval  50103  ranfval  50104