Theorem ovexi 7432

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

Syntax hints:   = wceq 1562   ∈ wcel 2144  Vcvv 3456  (class class class)co 7398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736  ax-nul 5258

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1565  df-fal 1575  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ne 2960  df-v 3458  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-sn 4585  df-pr 4587  df-uni 4868  df-iota 6479  df-fv 6531  df-ov 7401

This theorem is referenced by:  negex  11430  decex  12694  eulerthlem2  16819  subccatid  17881  funcres2c  17938  ressffth  17975  fuccofval  17997  fuchom  17999  fuccatid  18007  xpccatid  18222  gsumress  18718  prdssgrpd  18769  smndex1mgm  18946  eqgen  19224  quselbas  19227  quseccl0  19228  qus0subgbas  19241  orbsta  19355  sylow2blem1  19662  sylow2blem2  19663  frgpnabllem1  19915  rngqipbas  21367  rngqiprngimf  21369  rngqiprngghm  21371  rngqiprngimf1  21372  rngqiprnglin  21374  rngqiprngim  21376  rngqiprngfulem1  21383  znle  21590  znbas  21597  znzrhval  21600  relt  21669  retos  21672  frlmlbs  21851  lsslindf  21884  lsslinds  21885  uvcendim  21901  subrgmvr  22088  opsrle  22102  subrgascl  22121  evl1fval  22393  evls1vsca  22438  asclply1subcl  22439  matgsum  22499  matmulr  22500  scmatghm  22595  marepvfval  22627  m2cpmmhm  22807  cpm2mfval  22811  cpmadumatpolylem2  22944  cldsubg  24173  nghmfval  24784  pi1bas  25102  dv11cn  26065  quotval  26358  pserdvlem2  26493  ang180lem3  26878  dchrptlem2  27331  usgrexmpllem  29463  usgrexmpl  29466  nbusgrf1o1  29573  crctcshlem3  30021  2pthon3v  30145  konigsberglem5  30460  konigsberg  30461  bloval  30986  dpval  33069  fzo0pmtrlast  33274  rlocbas  33451  rloccring  33454  rloc0g  33455  rloc1r  33456  rlocf1  33457  rlocinvunit  33458  rlocisunit  33459  zringfrac  33752  resssra  33886  qusdimsum  33927  satfv1fvfmla1  35778  2goelgoanfmla1  35779  satefvfmla1  35780  cdleme31snd  41015  c0exALT  42873  prjcrvfval  43218  prjcrvval  43219  mnringmulrd  44804  subsalsal  46938  indprmfz  48244  isubgr3stgrlem2  48594  isubgr3stgrlem3  48595  isubgr3stgrlem5  48597  usgrexmpl1  48649  usgrexmpl1vtx  48650  usgrexmpl1edg  48651  usgrexmpl2  48654  usgrexmpl2vtx  48655  usgrexmpl2edg  48656  gpgvtx  48670  gpgiedg  48671  naryfvalixp  49256  naryfvalelfv  49259  rrxline  49361  inlinecirc02p  49414  inlinecirc02preu  49415  ssccatid  49698  resccatlem  49699