Theorem ovexi 7439

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  Vcvv 3459  (class class class)co 7405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-nul 5276

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-sn 4602  df-pr 4604  df-uni 4884  df-iota 6484  df-fv 6539  df-ov 7408

This theorem is referenced by:  negex  11480  decex  12712  cshwsexaOLD  14843  eulerthlem2  16801  subccatid  17859  funcres2c  17916  ressffth  17953  fuccofval  17975  fuchom  17977  fuccatid  17985  xpccatid  18200  gsumress  18660  prdssgrpd  18711  smndex1mgm  18885  eqgen  19164  quselbas  19167  quseccl0  19168  qus0subgbas  19181  orbsta  19296  sylow2blem1  19601  sylow2blem2  19602  frgpnabllem1  19854  rngqipbas  21256  rngqiprngimf  21258  rngqiprngghm  21260  rngqiprngimf1  21261  rngqiprnglin  21263  rngqiprngim  21265  rngqiprngfulem1  21272  znle  21497  znbas  21504  znzrhval  21507  relt  21575  retos  21578  frlmlbs  21757  lsslindf  21790  lsslinds  21791  uvcendim  21807  subrgmvr  21991  opsrle  22005  subrgascl  22024  evl1fval  22266  evls1vsca  22311  asclply1subcl  22312  matgsum  22375  matmulr  22376  scmatghm  22471  marepvfval  22503  m2cpmmhm  22683  cpm2mfval  22687  cpmadumatpolylem2  22820  cldsubg  24049  nghmfval  24661  pi1bas  24989  dv11cn  25958  quotval  26252  pserdvlem2  26390  ang180lem3  26773  dchrptlem2  27228  usgrexmpllem  29239  usgrexmpl  29242  nbusgrf1o1  29349  crctcshlem3  29801  2pthon3v  29925  konigsberglem5  30237  konigsberg  30238  bloval  30762  dpval  32864  fzo0pmtrlast  33103  rlocbas  33262  rloccring  33265  rloc0g  33266  rloc1r  33267  rlocf1  33268  zringfrac  33569  resssra  33627  qusdimsum  33668  satfv1fvfmla1  35445  2goelgoanfmla1  35446  satefvfmla1  35447  cdleme31snd  40405  c0exALT  42303  prjcrvfval  42654  prjcrvval  42655  mnringmulrd  44247  subsalsal  46388  isubgr3stgrlem2  47979  isubgr3stgrlem3  47980  isubgr3stgrlem5  47982  usgrexmpl1  48026  usgrexmpl1vtx  48027  usgrexmpl1edg  48028  usgrexmpl2  48031  usgrexmpl2vtx  48032  usgrexmpl2edg  48033  gpgvtx  48047  gpgiedg  48048  naryfvalixp  48609  naryfvalelfv  48612  rrxline  48714  inlinecirc02p  48767  inlinecirc02preu  48768  ssccatid  49039  resccatlem  49040