Theorem elexd 3466

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442

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 3444

This theorem is referenced by:  ifexd  4530  rabexg  5284  reuhypd  5366  ideqg  5808  elrnmptg  5918  dmmptd  6645  elfvex  6877  funcnvmpt  6951  fvmptd3f  6965  fvmptdv2  6968  tpres  7157  ovmpodxf  7518  ovmpodf  7524  mptmpoopabbrd  8034  mptmpoopabbrdOLD  8035  offval22  8040  mptsuppd  8139  suppssov1  8149  suppssov2  8150  suppssfv  8154  ordtypelem9  9443  cantnfp1lem2  9600  cantnflem3  9612  cnfcomlem  9620  ttukeylem3  10433  mptnn0fsupp  13932  mptnn0fsuppr  13934  seqf1olem2  13977  rtrclreclem1  14992  rtrclreclem2  14994  fsumrlim  15746  strfv2d  17140  prdsval  17387  imasval  17444  qusval  17475  xpsfrnel  17495  xpsval  17503  cofuval  17818  resfval  17828  funcres2c  17839  setcval  18013  catcval  18036  estrcval  18059  estrres  18074  xpcval  18112  prfval  18134  curfval  18158  uncfval  18169  isposd  18257  pospropd  18260  ipodrsima  18476  gsumvalx  18613  prdssgrpd  18670  prdsmndd  18707  prds0g  18708  prdsgrpd  18992  prdsinvgd  18993  eqgval  19118  prdscmnd  19802  isunit  20321  isirred  20367  isrim0  20430  rngcval  20563  ringcval  20592  prdslmodd  20932  frlmphllem  21747  psrval  21883  mvrfval  21948  opsrval  22013  selvffval  22088  mhpfval  22093  mhpmulcl  22104  psdffval  22112  evl1maprhm  22335  mamufval  22348  mvmulfval  22498  islocfin  23473  elmptrab2  23784  alexsub  24001  tsmsval2  24086  prdsdsf  24323  prdsxmet  24325  itg2gt0  25729  itgfsum  25796  mtest  26381  sltsd  27776  seqsp1  28319  mirval  28739  israg  28781  perpln1  28794  perpln2  28795  isperp  28796  midf  28860  ismidb  28862  lmif  28869  islmib  28871  f1otrg  28955  f1otrge  28956  structtocusgr  29531  iswlkg  29699  unidifsnne  32623  iinabrex  32656  fdifsupp  32775  mgcoval  33079  fxpval  33259  elrgspnlem3  33338  rlocval  33353  subrdom  33379  fldgenval  33406  islbs5  33473  linds2eq  33474  elrspunidl  33521  extvval  33708  splyval  33736  esplyval  33739  resssra  33764  exsslsb  33774  irngval  33863  minplyval  33883  algextdeglem4  33898  constrextdg2lem  33926  constrext2chnlem  33928  rhmpreimacnlem  34062  ofcfval  34276  sitgval  34510  breprexplema  34808  lpadval  34854  bnj1463  35231  fineqvrep  35292  fineqvpow  35293  fineqvnttrclse  35302  wevgblacfn  35325  wsuclem  36039  bj-inexeqex  37409  bj-idreseq  37417  bj-idreseqb  37418  bj-ideqg1ALT  37420  bj-imdirvallem  37435  opelopab3  37969  aks6d1c6lem2  42541  aks5lem2  42557  onsupex3  43591  pren2d  43912  frege81d  44103  frege129d  44119  rfovd  44357  fsovd  44364  fsovrfovd  44365  dssmapfvd  44373  rr-spce  44560  mnringvald  44569  grurankcld  44589  mnurnd  44639  dmmptdff  45581  dmmptdf2  45591  limsupequzmpt2  46076  liminfequzmpt2  46149  xlimliminflimsup  46220  rrxsnicc  46658  ioorrnopnlem  46662  ioorrnopnxrlem  46664  subsaliuncl  46716  sge0xaddlem1  46791  sge0xaddlem2  46792  sge0xadd  46793  sge0splitsn  46799  meaiininclem  46844  hoicvrrex  46914  ovn0lem  46923  hoidmvlelem3  46955  ovnhoilem1  46959  hoicoto2  46963  hoidifhspval3  46977  hoiqssbllem1  46980  ovolval4lem1  47007  vonvolmbl  47019  iinhoiicclem  47031  iunhoiioolem  47033  vonioolem1  47038  vonioolem2  47039  vonicclem1  47041  vonicclem2  47042  decsmf  47125  smflimlem4  47132  smfmullem4  47152  smfco  47160  smfpimcclem  47165  smflimsupmpt  47187  smfliminfmpt  47190  opabresex0d  47645  setsnidel  47737  isupwlkg  48497  isprsd  49314  initc  49450  funcoppc2  49502  swapfval  49621  fucofvalg  49677  prcofvalg  49735  lanfval  49972  ranfval  49973