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  4504  rabexg  5266  reuhypd  5349  ideqg  5794  elrnmptg  5904  dmmptd  6631  elfvex  6863  funcnvmpt  6938  fvmptd3f  6952  fvmptdv2  6955  tpres  7146  ovmpodxf  7507  ovmpodf  7513  mptmpoopabbrd  8023  offval22  8028  mptsuppd  8128  suppssov1  8138  suppssov2  8139  suppssfv  8143  ordtypelem9  9432  cantnfp1lem2  9592  cantnflem3  9604  cnfcomlem  9612  ttukeylem3  10425  mptnn0fsupp  13951  mptnn0fsuppr  13953  seqf1olem2  13996  rtrclreclem1  15011  rtrclreclem2  15013  fsumrlim  15766  strfv2d  17163  prdsval  17410  imasval  17467  qusval  17498  xpsfrnel  17518  xpsval  17526  cofuval  17841  resfval  17851  funcres2c  17862  setcval  18036  catcval  18059  estrcval  18082  estrres  18097  xpcval  18135  prfval  18157  curfval  18181  uncfval  18192  isposd  18280  pospropd  18283  ipodrsima  18499  gsumvalx  18636  prdssgrpd  18693  prdsmndd  18730  prds0g  18731  prdsgrpd  19018  prdsinvgd  19019  eqgval  19144  prdscmnd  19828  isunit  20345  isirred  20391  isrim0  20454  rngcval  20591  ringcval  20620  prdslmodd  20960  frlmphllem  21756  psrval  21891  mvrfval  21956  opsrval  22023  selvffval  22095  mhpfval  22127  mhpmulcl  22138  psdffval  22146  evl1maprhm  22366  mamufval  22376  mvmulfval  22526  islocfin  23501  elmptrab2  23812  alexsub  24029  tsmsval2  24114  prdsdsf  24351  prdsxmet  24353  itg2gt0  25746  itgfsum  25813  mtest  26388  sltsd  27779  seqsp1  28322  mirval  28742  israg  28784  perpln1  28797  perpln2  28798  isperp  28799  midf  28863  ismidb  28865  lmif  28872  islmib  28874  f1otrg  28958  f1otrge  28959  structtocusgr  29534  iswlkg  29701  unidifsnne  32625  iinabrex  32659  fdifsupp  32778  mgcoval  33066  fxpval  33247  elrgspnlem3  33326  rlocval  33341  subrdom  33367  fldgenval  33397  islbs5  33464  linds2eq  33465  elrspunidl  33512  0mplrim  33707  extvval  33724  splyval  33752  esplyval  33755  resssra  33780  exsslsb  33790  irngval  33878  minplyval  33898  algextdeglem4  33913  constrextdg2lem  33941  constrext2chnlem  33943  rhmpreimacnlem  34077  ofcfval  34291  sitgval  34525  breprexplema  34823  lpadval  34869  bnj1463  35246  fineqvrep  35304  fineqvpow  35305  fineqvnttrclse  35314  wevgblacfn  35346  wsuclem  36060  bj-inexeqex  37523  bj-idreseq  37531  bj-idreseqb  37532  bj-ideqg1ALT  37534  bj-imdirvallem  37549  opelopab3  38094  aks6d1c6lem2  42665  aks5lem2  42681  onsupex3  43688  pren2d  44009  frege81d  44200  frege129d  44216  rfovd  44454  fsovd  44461  fsovrfovd  44462  dssmapfvd  44470  rr-spce  44657  mnringvald  44666  grurankcld  44686  mnurnd  44736  dmmptdff  45676  dmmptdf2  45685  limsupequzmpt2  46169  liminfequzmpt2  46242  xlimliminflimsup  46313  rrxsnicc  46751  ioorrnopnlem  46755  ioorrnopnxrlem  46757  subsaliuncl  46809  sge0xaddlem1  46884  sge0xaddlem2  46885  sge0xadd  46886  sge0splitsn  46892  meaiininclem  46937  hoicvrrex  47007  ovn0lem  47016  hoidmvlelem3  47048  ovnhoilem1  47052  hoicoto2  47056  hoidifhspval3  47070  hoiqssbllem1  47073  ovolval4lem1  47100  vonvolmbl  47112  iinhoiicclem  47124  iunhoiioolem  47126  vonioolem1  47131  vonioolem2  47132  vonicclem1  47134  vonicclem2  47135  decsmf  47218  smflimlem4  47225  smfmullem4  47245  smfco  47253  smfpimcclem  47258  smflimsupmpt  47280  smfliminfmpt  47283  opabresex0d  47756  setsnidel  47860  isupwlkg  48636  isprsd  49453  initc  49589  funcoppc2  49641  swapfval  49760  fucofvalg  49816  prcofvalg  49874  lanfval  50111  ranfval  50112