Theorem elexd 3487

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

Syntax hints:   → wi 4   ∈ wcel 2098  Vcvv 3466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468

This theorem is referenced by:  ifexd  4568  reuhypd  5407  ideqg  5841  elrnmptg  5948  dmmptd  6685  elfvex  6919  fvmptd3f  7003  fvmptdv2  7006  tpres  7194  ovmpodxf  7550  ovmpodf  7556  mptmpoopabbrd  8060  mptmpoopabbrdOLD  8061  offval22  8068  mptsuppd  8166  suppssov1  8177  suppssov2  8178  suppssfv  8182  ordtypelem9  9517  cantnfp1lem2  9670  cantnflem3  9682  cnfcomlem  9690  ttukeylem3  10502  mptnn0fsupp  13959  mptnn0fsuppr  13961  seqf1olem2  14005  rtrclreclem1  15001  rtrclreclem2  15003  fsumrlim  15754  strfv2d  17134  prdsval  17400  imasval  17456  qusval  17487  xpsfrnel  17507  xpsval  17515  cofuval  17831  resfval  17841  funcres2c  17853  setcval  18029  catcval  18052  estrcval  18077  estrres  18093  xpcval  18131  prfval  18153  curfval  18178  uncfval  18189  isposd  18278  pospropd  18282  ipodrsima  18496  gsumvalx  18599  prdssgrpd  18656  prdsmndd  18690  prds0g  18691  prdsgrpd  18968  prdsinvgd  18969  eqgval  19094  prdscmnd  19771  isunit  20265  isirred  20311  isrim0  20375  rngcval  20504  ringcval  20533  prdslmodd  20806  frlmphllem  21643  psrval  21777  mvrfval  21850  opsrval  21911  selvffval  21986  mhpfval  21990  mhpmulcl  22000  psdffval  22008  mamufval  22209  mvmulfval  22366  islocfin  23343  elmptrab2  23654  alexsub  23871  tsmsval2  23956  prdsdsf  24195  prdsxmet  24197  itg2gt0  25612  itgfsum  25678  mtest  26257  ssltd  27640  seqsp1  28100  mirval  28375  israg  28417  perpln1  28430  perpln2  28431  isperp  28432  midf  28496  ismidb  28498  lmif  28505  islmib  28507  f1otrg  28591  f1otrge  28592  structtocusgr  29172  iswlkg  29339  unidifsnne  32242  iinabrex  32269  funcnvmpt  32361  mgcoval  32623  fldgenval  32868  islbs5  32965  linds2eq  32966  elrspunidl  33015  resssra  33153  irngval  33229  minplyval  33246  algextdeglem4  33256  rhmpreimacnlem  33353  ofcfval  33585  sitgval  33820  breprexplema  34131  lpadval  34177  bnj1463  34555  fineqvrep  34584  fineqvpow  34585  wsuclem  35292  bj-inexeqex  36525  bj-idreseq  36533  bj-idreseqb  36534  bj-ideqg1ALT  36536  bj-imdirvallem  36551  opelopab3  37076  onsupex3  42472  pren2d  42796  frege81d  42987  frege129d  43003  rfovd  43241  fsovd  43248  fsovrfovd  43249  dssmapfvd  43257  rr-spce  43445  mnringvald  43456  grurankcld  43481  mnurnd  43531  dmmptdff  44407  dmmptdf2  44420  limsupequzmpt2  44919  limsupvaluz2  44939  liminfequzmpt2  44992  xlimliminflimsup  45063  rrxsnicc  45501  ioorrnopnlem  45505  ioorrnopnxrlem  45507  subsaliuncl  45559  sge0xaddlem1  45634  sge0xaddlem2  45635  sge0xadd  45636  sge0splitsn  45642  meaiininclem  45687  hoicvrrex  45757  ovn0lem  45766  hoidmvlelem3  45798  ovnhoilem1  45802  hoicoto2  45806  hoidifhspval3  45820  hoiqssbllem1  45823  ovolval4lem1  45850  vonvolmbl  45862  iinhoiicclem  45874  iunhoiioolem  45876  vonioolem1  45881  vonioolem2  45882  vonicclem1  45884  vonicclem2  45885  decsmf  45968  smflimlem4  45975  smfmullem4  45995  smfco  46003  smfpimcclem  46008  smflimsupmpt  46030  smfliminfmpt  46033  opabresex0d  46478  setsnidel  46530  isupwlkg  47000  isprsd  47776