Theorem elexd 3442

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

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424

This theorem is referenced by:  ifexd  4504  reuhypd  5337  ideqg  5749  elrnmptg  5857  dmmptd  6562  elfvex  6789  fvmptd3f  6872  fvmptdv2  6875  tpres  7058  ovmpodxf  7401  ovmpodf  7407  offval22  7899  mptsuppd  7974  suppssov1  7985  suppssfv  7989  ordtypelem9  9215  cantnfp1lem2  9367  cantnflem3  9379  cnfcomlem  9387  ttukeylem3  10198  mptnn0fsupp  13645  mptnn0fsuppr  13647  seqf1olem2  13691  rtrclreclem1  14696  rtrclreclem2  14698  fsumrlim  15451  strfv2d  16831  prdsval  17083  imasval  17139  qusval  17170  xpsfrnel  17190  xpsval  17198  cofuval  17513  resfval  17523  funcres2c  17533  setcval  17708  catcval  17731  estrcval  17756  estrres  17772  xpcval  17810  prfval  17832  curfval  17857  uncfval  17868  isposd  17956  pospropd  17960  ipodrsima  18174  gsumvalx  18275  prdsmndd  18333  prds0g  18334  prdsgrpd  18600  prdsinvgd  18601  eqgval  18720  prdscmnd  19377  isunit  19814  isirred  19856  prdslmodd  20146  frlmphllem  20897  psrval  21028  mvrfval  21099  opsrval  21157  selvffval  21236  mhpfval  21239  mhpmulcl  21249  mamufval  21444  mvmulfval  21599  islocfin  22576  elmptrab2  22887  alexsub  23104  tsmsval2  23189  prdsdsf  23428  prdsxmet  23430  itg2gt0  24830  itgfsum  24896  mtest  25468  mirval  26920  israg  26962  perpln1  26975  perpln2  26976  isperp  26977  midf  27041  ismidb  27043  lmif  27050  islmib  27052  f1otrg  27136  f1otrge  27137  structtocusgr  27716  iswlkg  27883  unidifsnne  30785  iinabrex  30809  funcnvmpt  30906  mgcoval  31166  linds2eq  31477  elrspunidl  31508  rhmpreimacnlem  31736  ofcfval  31966  sitgval  32199  breprexplema  32510  lpadval  32556  bnj1463  32935  fineqvrep  32964  fineqvpow  32965  wsuclem  33746  ssltd  33913  bj-inexeqex  35252  bj-idreseq  35260  bj-idreseqb  35261  bj-ideqg1ALT  35263  bj-imdirvallem  35278  opelopab3  35802  pren2d  41052  frege81d  41244  frege129d  41260  rfovd  41498  fsovd  41505  fsovrfovd  41506  dssmapfvd  41514  rr-spce  41704  mnringvald  41715  grurankcld  41740  mnurnd  41790  dmmptdf  42652  dmmptdf2  42665  limsupequzmpt2  43149  limsupvaluz2  43169  liminfequzmpt2  43222  xlimliminflimsup  43293  rrxsnicc  43731  ioorrnopnlem  43735  ioorrnopnxrlem  43737  subsaliuncl  43787  sge0xaddlem1  43861  sge0xaddlem2  43862  sge0xadd  43863  sge0splitsn  43869  meaiininclem  43914  hoicvrrex  43984  ovn0lem  43993  hoidmvlelem3  44025  ovnhoilem1  44029  hoicoto2  44033  hoidifhspval3  44047  hoiqssbllem1  44050  ovolval4lem1  44077  vonvolmbl  44089  iinhoiicclem  44101  iunhoiioolem  44103  vonioolem1  44108  vonioolem2  44109  vonicclem1  44111  vonicclem2  44112  decsmf  44189  smflimlem4  44196  smfmullem4  44215  smfco  44223  smfpimcclem  44227  smflimsupmpt  44249  smfliminfmpt  44252  opabresex0d  44664  setsnidel  44717  isupwlkg  45187  rngcval  45408  ringcval  45454  isprsd  46137