Theorem ovexi 7424

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3450  (class class class)co 7390

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5264

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 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-sn 4593  df-pr 4595  df-uni 4875  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  negex  11426  decex  12660  cshwsexaOLD  14797  eulerthlem2  16759  subccatid  17815  funcres2c  17872  ressffth  17909  fuccofval  17931  fuchom  17933  fuccatid  17941  xpccatid  18156  gsumress  18616  prdssgrpd  18667  smndex1mgm  18841  eqgen  19120  quselbas  19123  quseccl0  19124  qus0subgbas  19137  orbsta  19252  sylow2blem1  19557  sylow2blem2  19558  frgpnabllem1  19810  rngqipbas  21212  rngqiprngimf  21214  rngqiprngghm  21216  rngqiprngimf1  21217  rngqiprnglin  21219  rngqiprngim  21221  rngqiprngfulem1  21228  znle  21453  znbas  21460  znzrhval  21463  relt  21531  retos  21534  frlmlbs  21713  lsslindf  21746  lsslinds  21747  uvcendim  21763  subrgmvr  21947  opsrle  21961  subrgascl  21980  evl1fval  22222  evls1vsca  22267  asclply1subcl  22268  matgsum  22331  matmulr  22332  scmatghm  22427  marepvfval  22459  m2cpmmhm  22639  cpm2mfval  22643  cpmadumatpolylem2  22776  cldsubg  24005  nghmfval  24617  pi1bas  24945  dv11cn  25913  quotval  26207  pserdvlem2  26345  ang180lem3  26728  dchrptlem2  27183  usgrexmpllem  29194  usgrexmpl  29197  nbusgrf1o1  29304  crctcshlem3  29756  2pthon3v  29880  konigsberglem5  30192  konigsberg  30193  bloval  30717  dpval  32817  fzo0pmtrlast  33056  rlocbas  33225  rloccring  33228  rloc0g  33229  rloc1r  33230  rlocf1  33231  zringfrac  33532  resssra  33590  qusdimsum  33631  satfv1fvfmla1  35417  2goelgoanfmla1  35418  satefvfmla1  35419  cdleme31snd  40387  c0exALT  42247  prjcrvfval  42626  prjcrvval  42627  mnringmulrd  44219  subsalsal  46364  isubgr3stgrlem2  47970  isubgr3stgrlem3  47971  isubgr3stgrlem5  47973  usgrexmpl1  48017  usgrexmpl1vtx  48018  usgrexmpl1edg  48019  usgrexmpl2  48022  usgrexmpl2vtx  48023  usgrexmpl2edg  48024  gpgvtx  48038  gpgiedg  48039  naryfvalixp  48622  naryfvalelfv  48625  rrxline  48727  inlinecirc02p  48780  inlinecirc02preu  48781  ssccatid  49065  resccatlem  49066