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 2837	1 ⊢ 𝐴 ∈ V

Syntax hints:   = wceq 1548   ∈ wcel 2121  Vcvv 3433  (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 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-nul 5231

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-v 3435  df-dif 3888  df-un 3890  df-ss 3902  df-nul 4265  df-sn 4559  df-pr 4561  df-uni 4842  df-iota 6445  df-fv 6497  df-ov 7363

This theorem is referenced by:  negex  11386  decex  12643  eulerthlem2  16747  subccatid  17808  funcres2c  17865  ressffth  17902  fuccofval  17924  fuchom  17926  fuccatid  17934  xpccatid  18149  gsumress  18645  prdssgrpd  18696  smndex1mgm  18873  eqgen  19151  quselbas  19154  quseccl0  19155  qus0subgbas  19168  orbsta  19283  sylow2blem1  19590  sylow2blem2  19591  frgpnabllem1  19843  rngqipbas  21292  rngqiprngimf  21294  rngqiprngghm  21296  rngqiprngimf1  21297  rngqiprnglin  21299  rngqiprngim  21301  rngqiprngfulem1  21308  znle  21515  znbas  21522  znzrhval  21525  relt  21594  retos  21597  frlmlbs  21776  lsslindf  21809  lsslinds  21810  uvcendim  21826  subrgmvr  22013  opsrle  22027  subrgascl  22046  evl1fval  22318  evls1vsca  22363  asclply1subcl  22364  matgsum  22424  matmulr  22425  scmatghm  22520  marepvfval  22552  m2cpmmhm  22732  cpm2mfval  22736  cpmadumatpolylem2  22869  cldsubg  24098  nghmfval  24709  pi1bas  25027  dv11cn  25990  quotval  26280  pserdvlem2  26415  ang180lem3  26797  dchrptlem2  27250  usgrexmpllem  29351  usgrexmpl  29354  nbusgrf1o1  29461  crctcshlem3  29909  2pthon3v  30033  konigsberglem5  30348  konigsberg  30349  bloval  30874  dpval  32972  fzo0pmtrlast  33177  rlocbas  33352  rloccring  33355  rloc0g  33356  rloc1r  33357  rlocf1  33358  zringfrac  33649  resssra  33783  qusdimsum  33824  satfv1fvfmla1  35666  2goelgoanfmla1  35667  satefvfmla1  35668  cdleme31snd  40893  c0exALT  42751  prjcrvfval  43096  prjcrvval  43097  mnringmulrd  44682  subsalsal  46816  indprmfz  48122  isubgr3stgrlem2  48472  isubgr3stgrlem3  48473  isubgr3stgrlem5  48475  usgrexmpl1  48527  usgrexmpl1vtx  48528  usgrexmpl1edg  48529  usgrexmpl2  48532  usgrexmpl2vtx  48533  usgrexmpl2edg  48534  gpgvtx  48548  gpgiedg  48549  naryfvalixp  49134  naryfvalelfv  49137  rrxline  49239  inlinecirc02p  49292  inlinecirc02preu  49293  ssccatid  49576  resccatlem  49577