Theorem ovexi 7383

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3436  (class class class)co 7349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5245

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-sn 4578  df-pr 4580  df-uni 4859  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  negex  11361  decex  12595  cshwsexaOLD  14731  eulerthlem2  16693  subccatid  17753  funcres2c  17810  ressffth  17847  fuccofval  17869  fuchom  17871  fuccatid  17879  xpccatid  18094  gsumress  18556  prdssgrpd  18607  smndex1mgm  18781  eqgen  19060  quselbas  19063  quseccl0  19064  qus0subgbas  19077  orbsta  19192  sylow2blem1  19499  sylow2blem2  19500  frgpnabllem1  19752  rngqipbas  21202  rngqiprngimf  21204  rngqiprngghm  21206  rngqiprngimf1  21207  rngqiprnglin  21209  rngqiprngim  21211  rngqiprngfulem1  21218  znle  21443  znbas  21450  znzrhval  21453  relt  21522  retos  21525  frlmlbs  21704  lsslindf  21737  lsslinds  21738  uvcendim  21754  subrgmvr  21938  opsrle  21952  subrgascl  21971  evl1fval  22213  evls1vsca  22258  asclply1subcl  22259  matgsum  22322  matmulr  22323  scmatghm  22418  marepvfval  22450  m2cpmmhm  22630  cpm2mfval  22634  cpmadumatpolylem2  22767  cldsubg  23996  nghmfval  24608  pi1bas  24936  dv11cn  25904  quotval  26198  pserdvlem2  26336  ang180lem3  26719  dchrptlem2  27174  usgrexmpllem  29205  usgrexmpl  29208  nbusgrf1o1  29315  crctcshlem3  29764  2pthon3v  29888  konigsberglem5  30200  konigsberg  30201  bloval  30725  dpval  32831  fzo0pmtrlast  33035  rlocbas  33208  rloccring  33211  rloc0g  33212  rloc1r  33213  rlocf1  33214  zringfrac  33492  resssra  33559  qusdimsum  33601  satfv1fvfmla1  35406  2goelgoanfmla1  35407  satefvfmla1  35408  cdleme31snd  40375  c0exALT  42235  prjcrvfval  42614  prjcrvval  42615  mnringmulrd  44206  subsalsal  46350  isubgr3stgrlem2  47961  isubgr3stgrlem3  47962  isubgr3stgrlem5  47964  usgrexmpl1  48016  usgrexmpl1vtx  48017  usgrexmpl1edg  48018  usgrexmpl2  48021  usgrexmpl2vtx  48022  usgrexmpl2edg  48023  gpgvtx  48037  gpgiedg  48038  naryfvalixp  48624  naryfvalelfv  48627  rrxline  48729  inlinecirc02p  48782  inlinecirc02preu  48783  ssccatid  49067  resccatlem  49068