Theorem ovexi 7464

Description: The result of an operation is a set. (Contributed by Glauco Siliprandi, 26-Jun-2021.)

Hypothesis

Ref	Expression
ovexi.1	⊢ 𝐴 = (𝐵𝐹𝐶)

Assertion

Ref	Expression
ovexi	⊢ 𝐴 ∈ V

Proof of Theorem ovexi

Step	Hyp	Ref	Expression
1		ovexi.1	. 2 ⊢ 𝐴 = (𝐵𝐹𝐶)
2		ovex 7463	. 2 ⊢ (𝐵𝐹𝐶) ∈ V
3	1, 2	eqeltri 2834	1 ⊢ 𝐴 ∈ V

Syntax hints:   = wceq 1536   ∈ wcel 2105  Vcvv 3477  (class class class)co 7430

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  ax-nul 5311

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-sn 4631  df-pr 4633  df-uni 4912  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  negex  11503  decex  12734  cshwsexaOLD  14859  eulerthlem2  16815  subccatid  17896  funcres2c  17954  ressffth  17991  fuccofval  18014  fuchom  18016  fuchomOLD  18017  fuccatid  18025  xpccatid  18243  gsumress  18707  prdssgrpd  18758  smndex1mgm  18932  eqgen  19211  quselbas  19214  quseccl0  19215  qus0subgbas  19228  orbsta  19343  sylow2blem1  19652  sylow2blem2  19653  frgpnabllem1  19905  rngqipbas  21322  rngqiprngimf  21324  rngqiprngghm  21326  rngqiprngimf1  21327  rngqiprnglin  21329  rngqiprngim  21331  rngqiprngfulem1  21338  znle  21568  znbas  21579  znzrhval  21582  relt  21650  retos  21653  frlmlbs  21834  lsslindf  21867  lsslinds  21868  uvcendim  21884  subrgmvr  22068  opsrle  22082  subrgascl  22107  evl1fval  22347  evls1vsca  22392  asclply1subcl  22393  matgsum  22458  matmulr  22459  scmatghm  22554  marepvfval  22586  m2cpmmhm  22766  cpm2mfval  22770  cpmadumatpolylem2  22903  cldsubg  24134  nghmfval  24758  pi1bas  25084  dv11cn  26054  quotval  26348  pserdvlem2  26486  ang180lem3  26868  dchrptlem2  27323  usgrexmpllem  29291  usgrexmpl  29294  nbusgrf1o1  29401  crctcshlem3  29848  2pthon3v  29972  konigsberglem5  30284  konigsberg  30285  bloval  30809  dpval  32856  fzo0pmtrlast  33094  rlocbas  33253  rloccring  33256  rloc0g  33257  rloc1r  33258  rlocf1  33259  zringfrac  33561  resssra  33616  qusdimsum  33655  satfv1fvfmla1  35407  2goelgoanfmla1  35408  satefvfmla1  35409  cdleme31snd  40368  c0exALT  42271  prjcrvfval  42617  prjcrvval  42618  mnringmulrd  44216  subsalsal  46314  isubgr3stgrlem2  47869  isubgr3stgrlem3  47870  isubgr3stgrlem5  47872  usgrexmpl1  47916  usgrexmpl1vtx  47917  usgrexmpl1edg  47918  usgrexmpl2  47921  usgrexmpl2vtx  47922  usgrexmpl2edg  47923  gpgvtx  47937  gpgiedg  47938  naryfvalixp  48478  naryfvalelfv  48481  rrxline  48583  inlinecirc02p  48636  inlinecirc02preu  48637