Theorem ovexi 7309

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

Syntax hints:   = wceq 1539   ∈ wcel 2106  Vcvv 3432  (class class class)co 7275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-nul 5230

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-sn 4562  df-pr 4564  df-uni 4840  df-iota 6391  df-fv 6441  df-ov 7278

This theorem is referenced by:  negex  11219  decex  12441  cshwsexa  14537  eulerthlem2  16483  subccatid  17561  funcres2c  17617  ressffth  17654  fuccofval  17676  fuchom  17678  fuchomOLD  17679  fuccatid  17687  xpccatid  17905  gsumress  18366  smndex1mgm  18546  eqgen  18809  orbsta  18919  sylow2blem1  19225  sylow2blem2  19226  frgpnabllem1  19474  znle  20740  znbas  20751  znzrhval  20754  relt  20820  retos  20823  frlmlbs  21004  lsslindf  21037  lsslinds  21038  uvcendim  21054  subrgmvr  21234  opsrle  21248  subrgascl  21274  evl1fval  21494  matgsum  21586  matmulr  21587  scmatghm  21682  marepvfval  21714  m2cpmmhm  21894  cpm2mfval  21898  cpmadumatpolylem2  22031  cldsubg  23262  nghmfval  23886  pi1bas  24201  dv11cn  25165  quotval  25452  pserdvlem2  25587  ang180lem3  25961  dchrptlem2  26413  usgrexmpllem  27627  nbusgrf1o1  27737  crctcshlem3  28184  2pthon3v  28308  konigsberglem5  28620  konigsberg  28621  bloval  29143  dpval  31164  qusdimsum  31709  satfv1fvfmla1  33385  2goelgoanfmla1  33386  satefvfmla1  33387  cdleme31snd  38400  c0exALT  40289  prjcrvfval  40468  prjcrvval  40469  mnringmulrd  41839  subsalsal  43898  naryfvalixp  45975  naryfvalelfv  45978  rrxline  46080  inlinecirc02p  46133  inlinecirc02preu  46134