Theorem ovexi 7421

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3447  (class class class)co 7387

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 2701  ax-nul 5261

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-sn 4590  df-pr 4592  df-uni 4872  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  negex  11419  decex  12653  cshwsexaOLD  14790  eulerthlem2  16752  subccatid  17808  funcres2c  17865  ressffth  17902  fuccofval  17924  fuchom  17926  fuccatid  17934  xpccatid  18149  gsumress  18609  prdssgrpd  18660  smndex1mgm  18834  eqgen  19113  quselbas  19116  quseccl0  19117  qus0subgbas  19130  orbsta  19245  sylow2blem1  19550  sylow2blem2  19551  frgpnabllem1  19803  rngqipbas  21205  rngqiprngimf  21207  rngqiprngghm  21209  rngqiprngimf1  21210  rngqiprnglin  21212  rngqiprngim  21214  rngqiprngfulem1  21221  znle  21446  znbas  21453  znzrhval  21456  relt  21524  retos  21527  frlmlbs  21706  lsslindf  21739  lsslinds  21740  uvcendim  21756  subrgmvr  21940  opsrle  21954  subrgascl  21973  evl1fval  22215  evls1vsca  22260  asclply1subcl  22261  matgsum  22324  matmulr  22325  scmatghm  22420  marepvfval  22452  m2cpmmhm  22632  cpm2mfval  22636  cpmadumatpolylem2  22769  cldsubg  23998  nghmfval  24610  pi1bas  24938  dv11cn  25906  quotval  26200  pserdvlem2  26338  ang180lem3  26721  dchrptlem2  27176  usgrexmpllem  29187  usgrexmpl  29190  nbusgrf1o1  29297  crctcshlem3  29749  2pthon3v  29873  konigsberglem5  30185  konigsberg  30186  bloval  30710  dpval  32810  fzo0pmtrlast  33049  rlocbas  33218  rloccring  33221  rloc0g  33222  rloc1r  33223  rlocf1  33224  zringfrac  33525  resssra  33583  qusdimsum  33624  satfv1fvfmla1  35410  2goelgoanfmla1  35411  satefvfmla1  35412  cdleme31snd  40380  c0exALT  42240  prjcrvfval  42619  prjcrvval  42620  mnringmulrd  44212  subsalsal  46357  isubgr3stgrlem2  47966  isubgr3stgrlem3  47967  isubgr3stgrlem5  47969  usgrexmpl1  48013  usgrexmpl1vtx  48014  usgrexmpl1edg  48015  usgrexmpl2  48018  usgrexmpl2vtx  48019  usgrexmpl2edg  48020  gpgvtx  48034  gpgiedg  48035  naryfvalixp  48618  naryfvalelfv  48621  rrxline  48723  inlinecirc02p  48776  inlinecirc02preu  48777  ssccatid  49061  resccatlem  49062