Theorem elexd 3486

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

Syntax hints:   → wi 4   ∈ wcel 2149  Vcvv 3463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465

This theorem is referenced by:  ifexd  4538  rabexg  5305  reuhypd  5388  ideqg  5835  elrnmptg  5949  dmmptd  6678  elfvex  6914  funcnvmpt  6989  fvmptd3f  7003  fvmptdv2  7006  tpres  7197  ovmpodxf  7558  ovmpodf  7564  mptmpoopabbrd  8074  offval22  8079  mptsuppd  8179  suppssov1  8189  suppssov2  8190  suppssfv  8194  ordtypelem9  9484  cantnfp1lem2  9644  cantnflem3  9656  cnfcomlem  9664  ttukeylem3  10491  mptnn0fsupp  14029  mptnn0fsuppr  14031  seqf1olem2  14074  rtrclreclem1  15090  rtrclreclem2  15092  fsumrlim  15859  strfv2d  17257  prdsval  17504  imasval  17561  qusval  17592  xpsfrnel  17612  xpsval  17620  cofuval  17935  resfval  17945  funcres2c  17956  setcval  18130  catcval  18153  estrcval  18176  estrres  18191  xpcval  18229  prfval  18251  curfval  18275  uncfval  18286  isposd  18374  pospropd  18377  ipodrsima  18593  gsumvalx  18730  prdssgrpd  18787  prdsmndd  18824  prds0g  18825  prdsgrpd  19112  prdsinvgd  19113  eqgval  19241  prdscmnd  19927  isunit  20451  isirred  20497  isrim0  20560  rngcval  20699  ringcval  20728  prdslmodd  21064  frlmphllem  21895  psrval  22030  mvrfval  22095  opsrval  22162  selvffval  22234  mhpfval  22266  mhpmulcl  22277  psdffval  22285  evl1maprhm  22504  mamufval  22514  mvmulfval  22664  islocfin  23639  elmptrab2  23950  alexsub  24167  tsmsval2  24252  prdsdsf  24489  prdsxmet  24491  itg2gt0  25884  itgfsum  25951  mtest  26529  sltsd  27923  seqsp1  28466  mirval  28890  israg  28932  perpln1  28945  perpln2  28946  isperp  28947  tgplnfn  29011  plngval  29013  isplng  29014  midf  29039  ismidb  29041  lmif  29048  islmib  29050  brprlng  29139  f1otrg  29157  f1otrge  29158  structtocusgr  29733  iswlkg  29900  unidifsnne  32819  iinabrex  32851  fdifsupp  32967  mgcoval  33243  fxpval  33422  elrgspnlem3  33501  rlocval  33516  subrdom  33542  fldgenval  33572  islbs5  33633  linds2eq  33634  elrspunidl  33676  0mplrim  33845  extvval  33862  splyval  33890  esplyval  33893  resssra  33918  exsslsb  33928  irngval  34016  minplyval  34036  algextdeglem4  34051  constrextdg2lem  34079  constrext2chnlem  34081  rhmpreimacnlem  34215  ofcfval  34429  sitgval  34663  breprexplema  34958  lpadval  35007  bnj1463  35384  fineqvrep  35446  fineqvpow  35447  fineqvnttrclse  35456  wevgblacfn  35490  wsuclem  36210  bj-inexeqex  37681  bj-idreseq  37689  bj-idreseqb  37690  bj-ideqg1ALT  37692  bj-imdirvallem  37707  opelopab3  38252  aks6d1c6lem2  42823  aks5lem2  42839  onsupex3  43848  pren2d  44169  frege81d  44360  frege129d  44376  rfovd  44614  fsovd  44621  fsovrfovd  44622  dssmapfvd  44630  rr-spce  44815  mnringvald  44824  grurankcld  44844  mnurnd  44880  dmmptdff  45826  dmmptdf2  45835  limsupequzmpt2  46319  liminfequzmpt2  46392  xlimliminflimsup  46463  rrxsnicc  46901  ioorrnopnlem  46905  ioorrnopnxrlem  46907  subsaliuncl  46959  sge0xaddlem1  47034  sge0xaddlem2  47035  sge0xadd  47036  sge0splitsn  47042  meaiininclem  47087  hoicvrrex  47157  ovn0lem  47166  hoidmvlelem3  47198  ovnhoilem1  47202  hoicoto2  47206  hoidifhspval3  47220  hoiqssbllem1  47223  ovolval4lem1  47250  vonvolmbl  47262  iinhoiicclem  47274  iunhoiioolem  47276  vonioolem1  47281  vonioolem2  47282  vonicclem1  47284  vonicclem2  47285  decsmf  47368  smflimlem4  47375  smfmullem4  47395  smfco  47403  smfpimcclem  47408  smflimsupmpt  47430  smfliminfmpt  47433  opabresex0d  47906  setsnidel  48010  isupwlkg  48786  isprsd  49613  initc  49749  funcoppc2  49801  swapfval  49920  fucofvalg  49976  prcofvalg  50034  lanfval  50271  ranfval  50272