Theorem ovexi 7404

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 7403	. 2 ⊢ (𝐵𝐹𝐶) ∈ V
3	1, 2	eqeltri 2833	1 ⊢ 𝐴 ∈ V

Syntax hints:   = wceq 1542   ∈ wcel 2114  Vcvv 3442  (class class class)co 7370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5255

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-sn 4583  df-pr 4585  df-uni 4866  df-iota 6458  df-fv 6510  df-ov 7373

This theorem is referenced by:  negex  11392  decex  12625  eulerthlem2  16723  subccatid  17784  funcres2c  17841  ressffth  17878  fuccofval  17900  fuchom  17902  fuccatid  17910  xpccatid  18125  gsumress  18621  prdssgrpd  18672  smndex1mgm  18849  eqgen  19127  quselbas  19130  quseccl0  19131  qus0subgbas  19144  orbsta  19259  sylow2blem1  19566  sylow2blem2  19567  frgpnabllem1  19819  rngqipbas  21267  rngqiprngimf  21269  rngqiprngghm  21271  rngqiprngimf1  21272  rngqiprnglin  21274  rngqiprngim  21276  rngqiprngfulem1  21283  znle  21508  znbas  21515  znzrhval  21518  relt  21587  retos  21590  frlmlbs  21769  lsslindf  21802  lsslinds  21803  uvcendim  21819  subrgmvr  22005  opsrle  22019  subrgascl  22038  evl1fval  22289  evls1vsca  22334  asclply1subcl  22335  matgsum  22398  matmulr  22399  scmatghm  22494  marepvfval  22526  m2cpmmhm  22706  cpm2mfval  22710  cpmadumatpolylem2  22843  cldsubg  24072  nghmfval  24683  pi1bas  25011  dv11cn  25979  quotval  26273  pserdvlem2  26411  ang180lem3  26794  dchrptlem2  27249  usgrexmpllem  29351  usgrexmpl  29354  nbusgrf1o1  29461  crctcshlem3  29910  2pthon3v  30034  konigsberglem5  30349  konigsberg  30350  bloval  30875  dpval  32988  fzo0pmtrlast  33192  rlocbas  33367  rloccring  33370  rloc0g  33371  rloc1r  33372  rlocf1  33373  zringfrac  33653  resssra  33770  qusdimsum  33812  satfv1fvfmla1  35645  2goelgoanfmla1  35646  satefvfmla1  35647  cdleme31snd  40791  c0exALT  42651  prjcrvfval  43018  prjcrvval  43019  mnringmulrd  44608  subsalsal  46746  isubgr3stgrlem2  48356  isubgr3stgrlem3  48357  isubgr3stgrlem5  48359  usgrexmpl1  48411  usgrexmpl1vtx  48412  usgrexmpl1edg  48413  usgrexmpl2  48416  usgrexmpl2vtx  48417  usgrexmpl2edg  48418  gpgvtx  48432  gpgiedg  48433  naryfvalixp  49018  naryfvalelfv  49021  rrxline  49123  inlinecirc02p  49176  inlinecirc02preu  49177  ssccatid  49460  resccatlem  49461