Theorem ovexi 7482

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

Syntax hints:   = wceq 1537   ∈ wcel 2108  Vcvv 3488  (class class class)co 7448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-sn 4649  df-pr 4651  df-uni 4932  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  negex  11534  decex  12762  cshwsexaOLD  14873  eulerthlem2  16829  subccatid  17910  funcres2c  17968  ressffth  18005  fuccofval  18028  fuchom  18030  fuchomOLD  18031  fuccatid  18039  xpccatid  18257  gsumress  18720  prdssgrpd  18771  smndex1mgm  18942  eqgen  19221  quselbas  19224  quseccl0  19225  qus0subgbas  19238  orbsta  19353  sylow2blem1  19662  sylow2blem2  19663  frgpnabllem1  19915  rngqipbas  21328  rngqiprngimf  21330  rngqiprngghm  21332  rngqiprngimf1  21333  rngqiprnglin  21335  rngqiprngim  21337  rngqiprngfulem1  21344  znle  21574  znbas  21585  znzrhval  21588  relt  21656  retos  21659  frlmlbs  21840  lsslindf  21873  lsslinds  21874  uvcendim  21890  subrgmvr  22074  opsrle  22088  subrgascl  22113  evl1fval  22353  evls1vsca  22398  asclply1subcl  22399  matgsum  22464  matmulr  22465  scmatghm  22560  marepvfval  22592  m2cpmmhm  22772  cpm2mfval  22776  cpmadumatpolylem2  22909  cldsubg  24140  nghmfval  24764  pi1bas  25090  dv11cn  26060  quotval  26352  pserdvlem2  26490  ang180lem3  26872  dchrptlem2  27327  usgrexmpllem  29295  usgrexmpl  29298  nbusgrf1o1  29405  crctcshlem3  29852  2pthon3v  29976  konigsberglem5  30288  konigsberg  30289  bloval  30813  dpval  32854  fzo0pmtrlast  33085  rlocbas  33239  rloccring  33242  rloc0g  33243  rloc1r  33244  rlocf1  33245  zringfrac  33547  resssra  33602  qusdimsum  33641  satfv1fvfmla1  35391  2goelgoanfmla1  35392  satefvfmla1  35393  cdleme31snd  40343  c0exALT  42247  evlsvvvallem2  42517  evlsvvval  42518  prjcrvfval  42586  prjcrvval  42587  mnringmulrd  44190  subsalsal  46280  usgrexmpl1  47837  usgrexmpl1vtx  47838  usgrexmpl1edg  47839  usgrexmpl2  47842  usgrexmpl2vtx  47843  usgrexmpl2edg  47844  naryfvalixp  48363  naryfvalelfv  48366  rrxline  48468  inlinecirc02p  48521  inlinecirc02preu  48522