Theorem ovexi 7403

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3444  (class class class)co 7369

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 5256

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 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-sn 4586  df-pr 4588  df-uni 4868  df-iota 6452  df-fv 6507  df-ov 7372

This theorem is referenced by:  negex  11395  decex  12629  cshwsexaOLD  14766  eulerthlem2  16728  subccatid  17788  funcres2c  17845  ressffth  17882  fuccofval  17904  fuchom  17906  fuccatid  17914  xpccatid  18129  gsumress  18591  prdssgrpd  18642  smndex1mgm  18816  eqgen  19095  quselbas  19098  quseccl0  19099  qus0subgbas  19112  orbsta  19227  sylow2blem1  19534  sylow2blem2  19535  frgpnabllem1  19787  rngqipbas  21237  rngqiprngimf  21239  rngqiprngghm  21241  rngqiprngimf1  21242  rngqiprnglin  21244  rngqiprngim  21246  rngqiprngfulem1  21253  znle  21478  znbas  21485  znzrhval  21488  relt  21557  retos  21560  frlmlbs  21739  lsslindf  21772  lsslinds  21773  uvcendim  21789  subrgmvr  21973  opsrle  21987  subrgascl  22006  evl1fval  22248  evls1vsca  22293  asclply1subcl  22294  matgsum  22357  matmulr  22358  scmatghm  22453  marepvfval  22485  m2cpmmhm  22665  cpm2mfval  22669  cpmadumatpolylem2  22802  cldsubg  24031  nghmfval  24643  pi1bas  24971  dv11cn  25939  quotval  26233  pserdvlem2  26371  ang180lem3  26754  dchrptlem2  27209  usgrexmpllem  29240  usgrexmpl  29243  nbusgrf1o1  29350  crctcshlem3  29799  2pthon3v  29923  konigsberglem5  30235  konigsberg  30236  bloval  30760  dpval  32860  fzo0pmtrlast  33064  rlocbas  33234  rloccring  33237  rloc0g  33238  rloc1r  33239  rlocf1  33240  zringfrac  33518  resssra  33576  qusdimsum  33617  satfv1fvfmla1  35403  2goelgoanfmla1  35404  satefvfmla1  35405  cdleme31snd  40373  c0exALT  42233  prjcrvfval  42612  prjcrvval  42613  mnringmulrd  44205  subsalsal  46350  isubgr3stgrlem2  47959  isubgr3stgrlem3  47960  isubgr3stgrlem5  47962  usgrexmpl1  48006  usgrexmpl1vtx  48007  usgrexmpl1edg  48008  usgrexmpl2  48011  usgrexmpl2vtx  48012  usgrexmpl2edg  48013  gpgvtx  48027  gpgiedg  48028  naryfvalixp  48611  naryfvalelfv  48614  rrxline  48716  inlinecirc02p  48769  inlinecirc02preu  48770  ssccatid  49054  resccatlem  49055