Theorem elexd 3474

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3451

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453

This theorem is used by:  ifexd  4531  rabexg  5299  reuhypd  5381  ideqg  5829  elrnmptg  5943  dmmptd  6682  elfvex  6918  funcnvmpt  6993  fvmptd3f  7007  fvmptdv2  7010  tpres  7205  ovmpodxf  7568  ovmpodf  7574  mpt3fvd  7686  mptmpoopabbrd  8092  offval22  8097  mptsuppd  8197  suppssov1  8207  suppssov2  8208  suppssfv  8212  ordtypelem9  9513  cantnfp1lem2  9673  cantnflem3  9685  cnfcomlem  9693  ttukeylem3  10582  mptnn0fsupp  14133  mptnn0fsuppr  14135  seqf1olem2  14178  rtrclreclem1  15203  rtrclreclem2  15205  fsumrlim  15971  strfv2d  17372  prdsval  17619  imasval  17676  qusval  17707  xpsfrnel  17727  xpsval  17735  cofuval  18050  resfval  18060  funcres2c  18071  setcval  18245  catcval  18268  estrcval  18291  estrres  18306  xpcval  18344  prfval  18366  curfval  18390  uncfval  18401  isposd  18489  pospropd  18492  ipodrsima  18708  gsumvalx  18858  prdssgrpd  18915  prdsmndd  18957  prds0g  18958  prdsgrpd  19253  prdsinvgd  19254  eqgval  19382  prdscmnd  20068  isunit  20596  isirred  20642  isrim0  20706  rngcval  20863  ringcval  20892  prdslmodd  21237  frlmphllem  22079  psrval  22216  mvrfval  22281  opsrval  22348  selvffval  22420  mhpfval  22452  mhpmulcl  22463  psdffval  22471  evl1maprhm  22690  mamufval  22700  mvmulfval  22850  islocfin  23829  elmptrab2  24140  alexsub  24357  tsmsval2  24442  prdsdsf  24679  prdsxmet  24681  itg2gt0  26074  itgfsum  26140  mtest  26724  sltsd  28147  seqsp1  28690  mirval  29120  israg  29165  perpln1  29178  perpln2  29179  isperp  29180  tgplnfn  29246  plngval  29248  isplng  29249  midf  29274  ismidb  29276  lmif  29283  islmib  29285  cgrabasimass  29371  brprlng  29409  f1otrg  29441  f1otrge  29442  structtocusgr  30020  iswlkg  30187  unidifsnne  33125  iinabrex  33156  fdifsupp  33271  mgcoval  33540  fxpval  33719  elrgspnlem3  33798  rlocval  33813  subrdom  33839  fldgenval  33867  islbs5  33928  linds2eq  33929  elrspunidl  33971  0mplrim  34139  extvval  34156  splyval  34184  esplyval  34187  resssra  34212  exsslsb  34222  irngval  34310  minplyval  34330  algextdeglem4  34345  constrextdg2lem  34373  constrext2chnlem  34375  rhmpreimacnlem  34509  ofcfval  34723  sitgval  34957  breprexplema  35252  lpadval  35301  bnj1463  35678  fineqvrep  35765  fineqvpow  35766  fineqvnttrclse  35775  wevgblacfn  35873  wsuclem  36567  bj-inexeqex  38055  bj-idreseq  38063  bj-idreseqb  38064  bj-ideqg1ALT  38066  bj-imdirvallem  38081  opelopab3  38632  aks6d1c6lem2  43201  aks5lem2  43217  onsupex3  44220  pren2d  44541  frege81d  44732  frege129d  44748  rfovd  44986  fsovd  44993  fsovrfovd  44994  dssmapfvd  45002  rr-spce  45187  mnringvald  45196  grurankcld  45216  mnurnd  45252  dmmptdff  46205  dmmptdf2  46214  limsupequzmpt2  46697  liminfequzmpt2  46770  xlimliminflimsup  46841  rrxsnicc  47279  ioorrnopnlem  47283  ioorrnopnxrlem  47285  subsaliuncl  47337  sge0xaddlem1  47412  sge0xaddlem2  47413  sge0xadd  47414  sge0splitsn  47420  meaiininclem  47465  hoicvrrex  47535  ovn0lem  47544  hoidmvlelem3  47576  ovnhoilem1  47580  hoicoto2  47584  hoidifhspval3  47598  hoiqssbllem1  47601  ovolval4lem1  47628  vonvolmbl  47640  iinhoiicclem  47652  iunhoiioolem  47654  vonioolem1  47659  vonioolem2  47660  vonicclem1  47662  vonicclem2  47663  decsmf  47746  smflimlem4  47753  smfmullem4  47773  smfco  47781  smfpimcclem  47786  smflimsupmpt  47808  smfliminfmpt  47811  opabresex0d  48324  setsnidel  48428  isupwlkg  49204  isprsd  50032  initc  50168  funcoppc2  50220  swapfval  50339  fucofvalg  50395  prcofvalg  50453  lanfval  50690  ranfval  50691