Theorem ovexi 7390

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  Vcvv 3438  (class class class)co 7356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-nul 5249

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-sn 4579  df-pr 4581  df-uni 4862  df-iota 6446  df-fv 6498  df-ov 7359

This theorem is referenced by:  negex  11376  decex  12609  eulerthlem2  16707  subccatid  17768  funcres2c  17825  ressffth  17862  fuccofval  17884  fuchom  17886  fuccatid  17894  xpccatid  18109  gsumress  18605  prdssgrpd  18656  smndex1mgm  18830  eqgen  19108  quselbas  19111  quseccl0  19112  qus0subgbas  19125  orbsta  19240  sylow2blem1  19547  sylow2blem2  19548  frgpnabllem1  19800  rngqipbas  21248  rngqiprngimf  21250  rngqiprngghm  21252  rngqiprngimf1  21253  rngqiprnglin  21255  rngqiprngim  21257  rngqiprngfulem1  21264  znle  21489  znbas  21496  znzrhval  21499  relt  21568  retos  21571  frlmlbs  21750  lsslindf  21783  lsslinds  21784  uvcendim  21800  subrgmvr  21986  opsrle  22000  subrgascl  22019  evl1fval  22270  evls1vsca  22315  asclply1subcl  22316  matgsum  22379  matmulr  22380  scmatghm  22475  marepvfval  22507  m2cpmmhm  22687  cpm2mfval  22691  cpmadumatpolylem2  22824  cldsubg  24053  nghmfval  24664  pi1bas  24992  dv11cn  25960  quotval  26254  pserdvlem2  26392  ang180lem3  26775  dchrptlem2  27230  usgrexmpllem  29282  usgrexmpl  29285  nbusgrf1o1  29392  crctcshlem3  29841  2pthon3v  29965  konigsberglem5  30280  konigsberg  30281  bloval  30805  dpval  32920  fzo0pmtrlast  33123  rlocbas  33298  rloccring  33301  rloc0g  33302  rloc1r  33303  rlocf1  33304  zringfrac  33584  resssra  33692  qusdimsum  33734  satfv1fvfmla1  35566  2goelgoanfmla1  35567  satefvfmla1  35568  cdleme31snd  40585  c0exALT  42449  prjcrvfval  42816  prjcrvval  42817  mnringmulrd  44406  subsalsal  46545  isubgr3stgrlem2  48155  isubgr3stgrlem3  48156  isubgr3stgrlem5  48158  usgrexmpl1  48210  usgrexmpl1vtx  48211  usgrexmpl1edg  48212  usgrexmpl2  48215  usgrexmpl2vtx  48216  usgrexmpl2edg  48217  gpgvtx  48231  gpgiedg  48232  naryfvalixp  48817  naryfvalelfv  48820  rrxline  48922  inlinecirc02p  48975  inlinecirc02preu  48976  ssccatid  49259  resccatlem  49260