Theorem elexd 3454

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432

This theorem is referenced by:  ifexd  4516  rabexg  5274  reuhypd  5356  ideqg  5800  elrnmptg  5910  dmmptd  6637  elfvex  6869  funcnvmpt  6943  fvmptd3f  6957  fvmptdv2  6960  tpres  7149  ovmpodxf  7510  ovmpodf  7516  mptmpoopabbrd  8026  offval22  8031  mptsuppd  8130  suppssov1  8140  suppssov2  8141  suppssfv  8145  ordtypelem9  9434  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  20586  ringcval  20615  prdslmodd  20955  frlmphllem  21770  psrval  21905  mvrfval  21969  opsrval  22034  selvffval  22109  mhpfval  22114  mhpmulcl  22125  psdffval  22133  evl1maprhm  22354  mamufval  22367  mvmulfval  22517  islocfin  23492  elmptrab2  23803  alexsub  24020  tsmsval2  24105  prdsdsf  24342  prdsxmet  24344  itg2gt0  25737  itgfsum  25804  mtest  26382  sltsd  27774  seqsp1  28317  mirval  28737  israg  28779  perpln1  28792  perpln2  28793  isperp  28794  midf  28858  ismidb  28860  lmif  28867  islmib  28869  f1otrg  28953  f1otrge  28954  structtocusgr  29529  iswlkg  29697  unidifsnne  32621  iinabrex  32654  fdifsupp  32773  mgcoval  33061  fxpval  33241  elrgspnlem3  33320  rlocval  33335  subrdom  33361  fldgenval  33388  islbs5  33455  linds2eq  33456  elrspunidl  33503  extvval  33690  splyval  33718  esplyval  33721  resssra  33746  exsslsb  33756  irngval  33845  minplyval  33865  algextdeglem4  33880  constrextdg2lem  33908  constrext2chnlem  33910  rhmpreimacnlem  34044  ofcfval  34258  sitgval  34492  breprexplema  34790  lpadval  34836  bnj1463  35213  fineqvrep  35274  fineqvpow  35275  fineqvnttrclse  35284  wevgblacfn  35307  wsuclem  36021  bj-inexeqex  37484  bj-idreseq  37492  bj-idreseqb  37493  bj-ideqg1ALT  37495  bj-imdirvallem  37510  opelopab3  38053  aks6d1c6lem2  42624  aks5lem2  42640  onsupex3  43680  pren2d  44001  frege81d  44192  frege129d  44208  rfovd  44446  fsovd  44453  fsovrfovd  44454  dssmapfvd  44462  rr-spce  44649  mnringvald  44658  grurankcld  44678  mnurnd  44728  dmmptdff  45670  dmmptdf2  45680  limsupequzmpt2  46164  liminfequzmpt2  46237  xlimliminflimsup  46308  rrxsnicc  46746  ioorrnopnlem  46750  ioorrnopnxrlem  46752  subsaliuncl  46804  sge0xaddlem1  46879  sge0xaddlem2  46880  sge0xadd  46881  sge0splitsn  46887  meaiininclem  46932  hoicvrrex  47002  ovn0lem  47011  hoidmvlelem3  47043  ovnhoilem1  47047  hoicoto2  47051  hoidifhspval3  47065  hoiqssbllem1  47068  ovolval4lem1  47095  vonvolmbl  47107  iinhoiicclem  47119  iunhoiioolem  47121  vonioolem1  47126  vonioolem2  47127  vonicclem1  47129  vonicclem2  47130  decsmf  47213  smflimlem4  47220  smfmullem4  47240  smfco  47248  smfpimcclem  47253  smflimsupmpt  47275  smfliminfmpt  47278  opabresex0d  47745  setsnidel  47849  isupwlkg  48625  isprsd  49442  initc  49578  funcoppc2  49630  swapfval  49749  fucofvalg  49805  prcofvalg  49863  lanfval  50100  ranfval  50101