Theorem ovexi 7401

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  Vcvv 3429  (class class class)co 7367

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 2708  ax-nul 5241

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-sn 4568  df-pr 4570  df-uni 4851  df-iota 6454  df-fv 6506  df-ov 7370

This theorem is referenced by:  negex  11391  decex  12648  eulerthlem2  16752  subccatid  17813  funcres2c  17870  ressffth  17907  fuccofval  17929  fuchom  17931  fuccatid  17939  xpccatid  18154  gsumress  18650  prdssgrpd  18701  smndex1mgm  18878  eqgen  19156  quselbas  19159  quseccl0  19160  qus0subgbas  19173  orbsta  19288  sylow2blem1  19595  sylow2blem2  19596  frgpnabllem1  19848  rngqipbas  21293  rngqiprngimf  21295  rngqiprngghm  21297  rngqiprngimf1  21298  rngqiprnglin  21300  rngqiprngim  21302  rngqiprngfulem1  21309  znle  21516  znbas  21523  znzrhval  21526  relt  21595  retos  21598  frlmlbs  21777  lsslindf  21810  lsslinds  21811  uvcendim  21827  subrgmvr  22011  opsrle  22025  subrgascl  22044  evl1fval  22293  evls1vsca  22338  asclply1subcl  22339  matgsum  22402  matmulr  22403  scmatghm  22498  marepvfval  22530  m2cpmmhm  22710  cpm2mfval  22714  cpmadumatpolylem2  22847  cldsubg  24076  nghmfval  24687  pi1bas  25005  dv11cn  25968  quotval  26258  pserdvlem2  26393  ang180lem3  26775  dchrptlem2  27228  usgrexmpllem  29329  usgrexmpl  29332  nbusgrf1o1  29439  crctcshlem3  29887  2pthon3v  30011  konigsberglem5  30326  konigsberg  30327  bloval  30852  dpval  32949  fzo0pmtrlast  33153  rlocbas  33328  rloccring  33331  rloc0g  33332  rloc1r  33333  rlocf1  33334  zringfrac  33614  resssra  33731  qusdimsum  33772  satfv1fvfmla1  35605  2goelgoanfmla1  35606  satefvfmla1  35607  cdleme31snd  40832  c0exALT  42691  prjcrvfval  43064  prjcrvval  43065  mnringmulrd  44650  subsalsal  46787  indprmfz  48093  isubgr3stgrlem2  48443  isubgr3stgrlem3  48444  isubgr3stgrlem5  48446  usgrexmpl1  48498  usgrexmpl1vtx  48499  usgrexmpl1edg  48500  usgrexmpl2  48503  usgrexmpl2vtx  48504  usgrexmpl2edg  48505  gpgvtx  48519  gpgiedg  48520  naryfvalixp  49105  naryfvalelfv  49108  rrxline  49210  inlinecirc02p  49263  inlinecirc02preu  49264  ssccatid  49547  resccatlem  49548