Theorem elexd 3501

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

Syntax hints:   → wi 4   ∈ wcel 2105  Vcvv 3477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479

This theorem is referenced by:  ifexd  4578  rabexg  5342  reuhypd  5424  ideqg  5864  elrnmptg  5974  dmmptd  6713  elfvex  6944  fvmptd3f  7030  fvmptdv2  7033  tpres  7220  ovmpodxf  7582  ovmpodf  7588  mptmpoopabbrd  8103  mptmpoopabbrdOLD  8104  offval22  8111  mptsuppd  8210  suppssov1  8220  suppssov2  8221  suppssfv  8225  ordtypelem9  9563  cantnfp1lem2  9716  cantnflem3  9728  cnfcomlem  9736  ttukeylem3  10548  mptnn0fsupp  14034  mptnn0fsuppr  14036  seqf1olem2  14079  rtrclreclem1  15092  rtrclreclem2  15094  fsumrlim  15843  strfv2d  17235  prdsval  17501  imasval  17557  qusval  17588  xpsfrnel  17608  xpsval  17616  cofuval  17932  resfval  17942  funcres2c  17954  setcval  18130  catcval  18153  estrcval  18178  estrres  18194  xpcval  18232  prfval  18254  curfval  18279  uncfval  18290  isposd  18380  pospropd  18384  ipodrsima  18598  gsumvalx  18701  prdssgrpd  18758  prdsmndd  18795  prds0g  18796  prdsgrpd  19080  prdsinvgd  19081  eqgval  19207  prdscmnd  19893  isunit  20389  isirred  20435  isrim0  20499  rngcval  20634  ringcval  20663  prdslmodd  20984  frlmphllem  21817  psrval  21952  mvrfval  22018  opsrval  22081  selvffval  22154  mhpfval  22159  mhpmulcl  22170  psdffval  22178  evl1maprhm  22398  mamufval  22411  mvmulfval  22563  islocfin  23540  elmptrab2  23851  alexsub  24068  tsmsval2  24153  prdsdsf  24392  prdsxmet  24394  itg2gt0  25809  itgfsum  25876  mtest  26461  ssltd  27850  seqsp1  28331  mirval  28677  israg  28719  perpln1  28732  perpln2  28733  isperp  28734  midf  28798  ismidb  28800  lmif  28807  islmib  28809  f1otrg  28893  f1otrge  28894  structtocusgr  29477  iswlkg  29645  unidifsnne  32561  iinabrex  32588  funcnvmpt  32683  fdifsupp  32699  mgcoval  32960  elrgspnlem3  33233  rlocval  33245  subrdom  33268  fldgenval  33293  islbs5  33387  linds2eq  33388  elrspunidl  33435  resssra  33616  irngval  33699  minplyval  33712  algextdeglem4  33725  rhmpreimacnlem  33844  ofcfval  34078  sitgval  34313  breprexplema  34623  lpadval  34669  bnj1463  35047  fineqvrep  35087  fineqvpow  35088  wevgblacfn  35092  wsuclem  35806  bj-inexeqex  37136  bj-idreseq  37144  bj-idreseqb  37145  bj-ideqg1ALT  37147  bj-imdirvallem  37162  opelopab3  37704  aks6d1c6lem2  42152  aks5lem2  42168  onsupex3  43222  pren2d  43545  frege81d  43736  frege129d  43752  rfovd  43990  fsovd  43997  fsovrfovd  43998  dssmapfvd  44006  rr-spce  44193  mnringvald  44203  grurankcld  44228  mnurnd  44278  dmmptdff  45165  dmmptdf2  45175  limsupequzmpt2  45673  liminfequzmpt2  45746  xlimliminflimsup  45817  rrxsnicc  46255  ioorrnopnlem  46259  ioorrnopnxrlem  46261  subsaliuncl  46313  sge0xaddlem1  46388  sge0xaddlem2  46389  sge0xadd  46390  sge0splitsn  46396  meaiininclem  46441  hoicvrrex  46511  ovn0lem  46520  hoidmvlelem3  46552  ovnhoilem1  46556  hoicoto2  46560  hoidifhspval3  46574  hoiqssbllem1  46577  ovolval4lem1  46604  vonvolmbl  46616  iinhoiicclem  46628  iunhoiioolem  46630  vonioolem1  46635  vonioolem2  46636  vonicclem1  46638  vonicclem2  46639  decsmf  46722  smflimlem4  46729  smfmullem4  46749  smfco  46757  smfpimcclem  46762  smflimsupmpt  46784  smfliminfmpt  46787  opabresex0d  47234  setsnidel  47301  isupwlkg  47980  isprsd  48751