Theorem ovexi 7289

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

Syntax hints:   = wceq 1539   ∈ wcel 2108  Vcvv 3422  (class class class)co 7255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-nul 5225

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-sn 4559  df-pr 4561  df-uni 4837  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  negex  11149  decex  12370  cshwsexa  14465  eulerthlem2  16411  subccatid  17477  funcres2c  17533  ressffth  17570  fuccofval  17592  fuchom  17594  fuchomOLD  17595  fuccatid  17603  xpccatid  17821  gsumress  18281  smndex1mgm  18461  eqgen  18724  orbsta  18834  sylow2blem1  19140  sylow2blem2  19141  frgpnabllem1  19389  znle  20652  znbas  20663  znzrhval  20666  relt  20732  retos  20735  frlmlbs  20914  lsslindf  20947  lsslinds  20948  uvcendim  20964  subrgmvr  21144  opsrle  21158  subrgascl  21184  evl1fval  21404  matgsum  21494  matmulr  21495  scmatghm  21590  marepvfval  21622  m2cpmmhm  21802  cpm2mfval  21806  cpmadumatpolylem2  21939  cldsubg  23170  nghmfval  23792  pi1bas  24107  dv11cn  25070  quotval  25357  pserdvlem2  25492  ang180lem3  25866  dchrptlem2  26318  usgrexmpllem  27530  nbusgrf1o1  27640  crctcshlem3  28085  2pthon3v  28209  konigsberglem5  28521  konigsberg  28522  bloval  29044  dpval  31066  qusdimsum  31611  satfv1fvfmla1  33285  2goelgoanfmla1  33286  satefvfmla1  33287  cdleme31snd  38327  c0exALT  40210  mnringmulrd  41728  subsalsal  43788  naryfvalixp  45863  naryfvalelfv  45866  rrxline  45968  inlinecirc02p  46021  inlinecirc02preu  46022