Theorem ovexi 7442

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

Syntax hints:   = wceq 1541   ∈ wcel 2106  Vcvv 3474  (class class class)co 7408

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-sn 4629  df-pr 4631  df-uni 4909  df-iota 6495  df-fv 6551  df-ov 7411

This theorem is referenced by:  negex  11457  decex  12680  cshwsexaOLD  14774  eulerthlem2  16714  subccatid  17795  funcres2c  17851  ressffth  17888  fuccofval  17910  fuchom  17912  fuchomOLD  17913  fuccatid  17921  xpccatid  18139  gsumress  18600  prdssgrpd  18623  smndex1mgm  18787  eqgen  19060  quselbas  19062  quseccl0  19063  qus0subgbas  19074  orbsta  19176  sylow2blem1  19487  sylow2blem2  19488  frgpnabllem1  19740  znle  21087  znbas  21098  znzrhval  21101  relt  21167  retos  21170  frlmlbs  21351  lsslindf  21384  lsslinds  21385  uvcendim  21401  subrgmvr  21587  opsrle  21601  subrgascl  21626  evl1fval  21846  matgsum  21938  matmulr  21939  scmatghm  22034  marepvfval  22066  m2cpmmhm  22246  cpm2mfval  22250  cpmadumatpolylem2  22383  cldsubg  23614  nghmfval  24238  pi1bas  24553  dv11cn  25517  quotval  25804  pserdvlem2  25939  ang180lem3  26313  dchrptlem2  26765  usgrexmpllem  28514  nbusgrf1o1  28624  crctcshlem3  29070  2pthon3v  29194  konigsberglem5  29506  konigsberg  29507  bloval  30029  dpval  32051  evls1vsca  32645  asclply1subcl  32655  qusdimsum  32708  satfv1fvfmla1  34409  2goelgoanfmla1  34410  satefvfmla1  34411  cdleme31snd  39252  evlsvvvallem2  41136  evlsvvval  41137  evlsmhpvvval  41169  mhphf  41171  c0exALT  41175  prjcrvfval  41374  prjcrvval  41375  mnringmulrd  42970  subsalsal  45065  rngqipbas  46770  rngqiprngimf  46772  rngqiprngghm  46774  rngqiprngimf1  46775  rngqiprnglin  46777  rngqiprngim  46779  rngqiprngfulem1  46786  naryfvalixp  47305  naryfvalelfv  47308  rrxline  47410  inlinecirc02p  47463  inlinecirc02preu  47464