Theorem ovexi 7465

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  Vcvv 3480  (class class class)co 7431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-sn 4627  df-pr 4629  df-uni 4908  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  negex  11506  decex  12737  cshwsexaOLD  14863  eulerthlem2  16819  subccatid  17891  funcres2c  17948  ressffth  17985  fuccofval  18007  fuchom  18009  fuccatid  18017  xpccatid  18233  gsumress  18695  prdssgrpd  18746  smndex1mgm  18920  eqgen  19199  quselbas  19202  quseccl0  19203  qus0subgbas  19216  orbsta  19331  sylow2blem1  19638  sylow2blem2  19639  frgpnabllem1  19891  rngqipbas  21305  rngqiprngimf  21307  rngqiprngghm  21309  rngqiprngimf1  21310  rngqiprnglin  21312  rngqiprngim  21314  rngqiprngfulem1  21321  znle  21551  znbas  21562  znzrhval  21565  relt  21633  retos  21636  frlmlbs  21817  lsslindf  21850  lsslinds  21851  uvcendim  21867  subrgmvr  22051  opsrle  22065  subrgascl  22090  evl1fval  22332  evls1vsca  22377  asclply1subcl  22378  matgsum  22443  matmulr  22444  scmatghm  22539  marepvfval  22571  m2cpmmhm  22751  cpm2mfval  22755  cpmadumatpolylem2  22888  cldsubg  24119  nghmfval  24743  pi1bas  25071  dv11cn  26040  quotval  26334  pserdvlem2  26472  ang180lem3  26854  dchrptlem2  27309  usgrexmpllem  29277  usgrexmpl  29280  nbusgrf1o1  29387  crctcshlem3  29839  2pthon3v  29963  konigsberglem5  30275  konigsberg  30276  bloval  30800  dpval  32872  fzo0pmtrlast  33112  rlocbas  33271  rloccring  33274  rloc0g  33275  rloc1r  33276  rlocf1  33277  zringfrac  33582  resssra  33638  qusdimsum  33679  satfv1fvfmla1  35428  2goelgoanfmla1  35429  satefvfmla1  35430  cdleme31snd  40388  c0exALT  42293  prjcrvfval  42641  prjcrvval  42642  mnringmulrd  44240  subsalsal  46374  isubgr3stgrlem2  47934  isubgr3stgrlem3  47935  isubgr3stgrlem5  47937  usgrexmpl1  47981  usgrexmpl1vtx  47982  usgrexmpl1edg  47983  usgrexmpl2  47986  usgrexmpl2vtx  47987  usgrexmpl2edg  47988  gpgvtx  48002  gpgiedg  48003  naryfvalixp  48550  naryfvalelfv  48553  rrxline  48655  inlinecirc02p  48708  inlinecirc02preu  48709