Theorem ovexi 7169

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

Syntax hints:   = wceq 1538   ∈ wcel 2111  Vcvv 3441  (class class class)co 7135

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-nul 5174

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-sn 4526  df-pr 4528  df-uni 4801  df-iota 6283  df-fv 6332  df-ov 7138

This theorem is referenced by:  negex  10873  decex  12090  cshwsexa  14177  eulerthlem2  16109  subccatid  17108  funcres2c  17163  ressffth  17200  fuccofval  17221  fuchom  17223  fuccatid  17231  xpccatid  17430  gsumress  17884  smndex1mgm  18064  eqgen  18325  orbsta  18435  sylow2blem1  18737  sylow2blem2  18738  frgpnabllem1  18986  znle  20228  znbas  20235  znzrhval  20238  relt  20304  retos  20307  frlmlbs  20486  lsslindf  20519  lsslinds  20520  uvcendim  20536  subrgmvr  20701  opsrle  20715  subrgascl  20737  evl1fval  20952  matgsum  21042  matmulr  21043  scmatghm  21138  marepvfval  21170  m2cpmmhm  21350  cpm2mfval  21354  cpmadumatpolylem2  21487  cldsubg  22716  nghmfval  23328  pi1bas  23643  dv11cn  24604  quotval  24888  pserdvlem2  25023  ang180lem3  25397  dchrptlem2  25849  usgrexmpllem  27050  nbusgrf1o1  27160  crctcshlem3  27605  2pthon3v  27729  konigsberglem5  28041  konigsberg  28042  bloval  28564  dpval  30592  qusdimsum  31112  satfv1fvfmla1  32783  2goelgoanfmla1  32784  satefvfmla1  32785  cdleme31snd  37682  c0exALT  39460  mnringmulrd  40931  subsalsal  42999  naryfvalixp  45043  naryfvalelfv  45046  rrxline  45148  inlinecirc02p  45201  inlinecirc02preu  45202