Theorem ovexi 7396

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  Vcvv 3430  (class class class)co 7362

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 5242

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 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-sn 4569  df-pr 4571  df-uni 4852  df-iota 6450  df-fv 6502  df-ov 7365

This theorem is referenced by:  negex  11386  decex  12643  eulerthlem2  16747  subccatid  17808  funcres2c  17865  ressffth  17902  fuccofval  17924  fuchom  17926  fuccatid  17934  xpccatid  18149  gsumress  18645  prdssgrpd  18696  smndex1mgm  18873  eqgen  19151  quselbas  19154  quseccl0  19155  qus0subgbas  19168  orbsta  19283  sylow2blem1  19590  sylow2blem2  19591  frgpnabllem1  19843  rngqipbas  21289  rngqiprngimf  21291  rngqiprngghm  21293  rngqiprngimf1  21294  rngqiprnglin  21296  rngqiprngim  21298  rngqiprngfulem1  21305  znle  21530  znbas  21537  znzrhval  21540  relt  21609  retos  21612  frlmlbs  21791  lsslindf  21824  lsslinds  21825  uvcendim  21841  subrgmvr  22025  opsrle  22039  subrgascl  22058  evl1fval  22307  evls1vsca  22352  asclply1subcl  22353  matgsum  22416  matmulr  22417  scmatghm  22512  marepvfval  22544  m2cpmmhm  22724  cpm2mfval  22728  cpmadumatpolylem2  22861  cldsubg  24090  nghmfval  24701  pi1bas  25019  dv11cn  25982  quotval  26273  pserdvlem2  26410  ang180lem3  26792  dchrptlem2  27246  usgrexmpllem  29347  usgrexmpl  29350  nbusgrf1o1  29457  crctcshlem3  29906  2pthon3v  30030  konigsberglem5  30345  konigsberg  30346  bloval  30871  dpval  32968  fzo0pmtrlast  33172  rlocbas  33347  rloccring  33350  rloc0g  33351  rloc1r  33352  rlocf1  33353  zringfrac  33633  resssra  33750  qusdimsum  33792  satfv1fvfmla1  35625  2goelgoanfmla1  35626  satefvfmla1  35627  cdleme31snd  40850  c0exALT  42709  prjcrvfval  43082  prjcrvval  43083  mnringmulrd  44672  subsalsal  46809  indprmfz  48109  isubgr3stgrlem2  48459  isubgr3stgrlem3  48460  isubgr3stgrlem5  48462  usgrexmpl1  48514  usgrexmpl1vtx  48515  usgrexmpl1edg  48516  usgrexmpl2  48519  usgrexmpl2vtx  48520  usgrexmpl2edg  48521  gpgvtx  48535  gpgiedg  48536  naryfvalixp  49121  naryfvalelfv  49124  rrxline  49226  inlinecirc02p  49279  inlinecirc02preu  49280  ssccatid  49563  resccatlem  49564