Theorem elexd 3504

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482

This theorem is referenced by:  ifexd  4574  rabexg  5337  reuhypd  5419  ideqg  5862  elrnmptg  5972  dmmptd  6713  elfvex  6944  fvmptd3f  7031  fvmptdv2  7034  tpres  7221  ovmpodxf  7583  ovmpodf  7589  mptmpoopabbrd  8105  mptmpoopabbrdOLD  8106  offval22  8113  mptsuppd  8212  suppssov1  8222  suppssov2  8223  suppssfv  8227  ordtypelem9  9566  cantnfp1lem2  9719  cantnflem3  9731  cnfcomlem  9739  ttukeylem3  10551  mptnn0fsupp  14038  mptnn0fsuppr  14040  seqf1olem2  14083  rtrclreclem1  15096  rtrclreclem2  15098  fsumrlim  15847  strfv2d  17238  prdsval  17500  imasval  17556  qusval  17587  xpsfrnel  17607  xpsval  17615  cofuval  17927  resfval  17937  funcres2c  17948  setcval  18122  catcval  18145  estrcval  18168  estrres  18184  xpcval  18222  prfval  18244  curfval  18268  uncfval  18279  isposd  18368  pospropd  18372  ipodrsima  18586  gsumvalx  18689  prdssgrpd  18746  prdsmndd  18783  prds0g  18784  prdsgrpd  19068  prdsinvgd  19069  eqgval  19195  prdscmnd  19879  isunit  20373  isirred  20419  isrim0  20483  rngcval  20618  ringcval  20647  prdslmodd  20967  frlmphllem  21800  psrval  21935  mvrfval  22001  opsrval  22064  selvffval  22137  mhpfval  22142  mhpmulcl  22153  psdffval  22161  evl1maprhm  22383  mamufval  22396  mvmulfval  22548  islocfin  23525  elmptrab2  23836  alexsub  24053  tsmsval2  24138  prdsdsf  24377  prdsxmet  24379  itg2gt0  25795  itgfsum  25862  mtest  26447  ssltd  27836  seqsp1  28317  mirval  28663  israg  28705  perpln1  28718  perpln2  28719  isperp  28720  midf  28784  ismidb  28786  lmif  28793  islmib  28795  f1otrg  28879  f1otrge  28880  structtocusgr  29463  iswlkg  29631  unidifsnne  32554  iinabrex  32582  funcnvmpt  32677  fdifsupp  32694  mgcoval  32976  elrgspnlem3  33248  rlocval  33263  subrdom  33288  fldgenval  33314  islbs5  33408  linds2eq  33409  elrspunidl  33456  resssra  33638  exsslsb  33647  irngval  33735  minplyval  33748  algextdeglem4  33761  constrextdg2lem  33789  rhmpreimacnlem  33883  ofcfval  34099  sitgval  34334  breprexplema  34645  lpadval  34691  bnj1463  35069  fineqvrep  35109  fineqvpow  35110  wevgblacfn  35114  wsuclem  35826  bj-inexeqex  37155  bj-idreseq  37163  bj-idreseqb  37164  bj-ideqg1ALT  37166  bj-imdirvallem  37181  opelopab3  37725  aks6d1c6lem2  42172  aks5lem2  42188  onsupex3  43246  pren2d  43569  frege81d  43760  frege129d  43776  rfovd  44014  fsovd  44021  fsovrfovd  44022  dssmapfvd  44030  rr-spce  44217  mnringvald  44227  grurankcld  44252  mnurnd  44302  dmmptdff  45228  dmmptdf2  45238  limsupequzmpt2  45733  liminfequzmpt2  45806  xlimliminflimsup  45877  rrxsnicc  46315  ioorrnopnlem  46319  ioorrnopnxrlem  46321  subsaliuncl  46373  sge0xaddlem1  46448  sge0xaddlem2  46449  sge0xadd  46450  sge0splitsn  46456  meaiininclem  46501  hoicvrrex  46571  ovn0lem  46580  hoidmvlelem3  46612  ovnhoilem1  46616  hoicoto2  46620  hoidifhspval3  46634  hoiqssbllem1  46637  ovolval4lem1  46664  vonvolmbl  46676  iinhoiicclem  46688  iunhoiioolem  46690  vonioolem1  46695  vonioolem2  46696  vonicclem1  46698  vonicclem2  46699  decsmf  46782  smflimlem4  46789  smfmullem4  46809  smfco  46817  smfpimcclem  46822  smflimsupmpt  46844  smfliminfmpt  46847  opabresex0d  47297  setsnidel  47364  isupwlkg  48053  isprsd  48852  swapfval  48968  fucofvalg  49013