Theorem ovexi 7394

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  Vcvv 3441  (class class class)co 7360

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 5252

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 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-sn 4582  df-pr 4584  df-uni 4865  df-iota 6449  df-fv 6501  df-ov 7363

This theorem is referenced by:  negex  11382  decex  12615  eulerthlem2  16713  subccatid  17774  funcres2c  17831  ressffth  17868  fuccofval  17890  fuchom  17892  fuccatid  17900  xpccatid  18115  gsumress  18611  prdssgrpd  18662  smndex1mgm  18836  eqgen  19114  quselbas  19117  quseccl0  19118  qus0subgbas  19131  orbsta  19246  sylow2blem1  19553  sylow2blem2  19554  frgpnabllem1  19806  rngqipbas  21254  rngqiprngimf  21256  rngqiprngghm  21258  rngqiprngimf1  21259  rngqiprnglin  21261  rngqiprngim  21263  rngqiprngfulem1  21270  znle  21495  znbas  21502  znzrhval  21505  relt  21574  retos  21577  frlmlbs  21756  lsslindf  21789  lsslinds  21790  uvcendim  21806  subrgmvr  21992  opsrle  22006  subrgascl  22025  evl1fval  22276  evls1vsca  22321  asclply1subcl  22322  matgsum  22385  matmulr  22386  scmatghm  22481  marepvfval  22513  m2cpmmhm  22693  cpm2mfval  22697  cpmadumatpolylem2  22830  cldsubg  24059  nghmfval  24670  pi1bas  24998  dv11cn  25966  quotval  26260  pserdvlem2  26398  ang180lem3  26781  dchrptlem2  27236  usgrexmpllem  29337  usgrexmpl  29340  nbusgrf1o1  29447  crctcshlem3  29896  2pthon3v  30020  konigsberglem5  30335  konigsberg  30336  bloval  30860  dpval  32973  fzo0pmtrlast  33176  rlocbas  33351  rloccring  33354  rloc0g  33355  rloc1r  33356  rlocf1  33357  zringfrac  33637  resssra  33745  qusdimsum  33787  satfv1fvfmla1  35619  2goelgoanfmla1  35620  satefvfmla1  35621  cdleme31snd  40714  c0exALT  42574  prjcrvfval  42941  prjcrvval  42942  mnringmulrd  44531  subsalsal  46670  isubgr3stgrlem2  48280  isubgr3stgrlem3  48281  isubgr3stgrlem5  48283  usgrexmpl1  48335  usgrexmpl1vtx  48336  usgrexmpl1edg  48337  usgrexmpl2  48340  usgrexmpl2vtx  48341  usgrexmpl2edg  48342  gpgvtx  48356  gpgiedg  48357  naryfvalixp  48942  naryfvalelfv  48945  rrxline  49047  inlinecirc02p  49100  inlinecirc02preu  49101  ssccatid  49384  resccatlem  49385