Theorem ovexi 7454

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  Vcvv 3451  (class class class)co 7420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-sn 4585  df-pr 4587  df-uni 4868  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  negex  11555  decex  12818  eulerthlem2  16959  subccatid  18021  funcres2c  18078  ressffth  18115  fuccofval  18137  fuchom  18139  fuccatid  18147  xpccatid  18362  gsumress  18871  prdssgrpd  18922  smndex1mgm  19106  eqgen  19393  quselbas  19399  quseccl0  19400  qus0subgbas  19413  orbsta  19527  sylow2blem1  19834  sylow2blem2  19835  frgpnabllem1  20087  rngqipbas  21591  rngqiprngimf  21593  rngqiprngghm  21595  rngqiprngimf1  21596  rngqiprnglin  21598  rngqiprngim  21600  rngqiprngfulem1  21607  znle  21842  znbas  21849  znzrhval  21852  relt  21921  retos  21924  frlmlbs  22103  lsslindf  22136  lsslinds  22137  uvcendim  22153  subrgmvr  22342  opsrle  22356  subrgascl  22375  evl1fval  22646  evls1vsca  22691  asclply1subcl  22692  matgsum  22752  matmulr  22753  scmatghm  22848  marepvfval  22880  m2cpmmhm  23063  cpm2mfval  23067  cpmadumatpolylem2  23200  cldsubg  24430  nghmfval  25041  pi1bas  25359  dv11cn  26321  quotval  26613  pserdvlem2  26755  ang180lem3  27139  dchrptlem2  27592  usgrexmpllem  29841  usgrexmpl  29844  nbusgrf1o1  29951  crctcshlem3  30408  2pthon3v  30532  konigsberglem5  30857  konigsberg  30858  bloval  31383  dpval  33456  fzo0pmtrlast  33653  rlocbas  33829  rloccring  33832  rloc0g  33833  rloc1r  33834  rlocf1  33835  rlocinvunit  33836  rlocisunit  33837  zringfrac  34086  resssra  34219  qusdimsum  34260  satfv1fvfmla1  36188  2goelgoanfmla1  36189  satefvfmla1  36190  cdleme31snd  41443  c0exALT  43303  prjcrvfval  43667  prjcrvval  43668  mnringmulrd  45220  subsalsal  47368  indprmfz  48714  isubgr3stgrlem2  49064  isubgr3stgrlem3  49065  isubgr3stgrlem5  49067  usgrexmpl1  49119  usgrexmpl1vtx  49120  usgrexmpl1edg  49121  usgrexmpl2  49124  usgrexmpl2vtx  49125  usgrexmpl2edg  49126  gpgvtx  49140  gpgiedg  49141  naryfvalixp  49740  naryfvalelfv  49743  rrxline  49845  inlinecirc02p  49898  inlinecirc02preu  49899  ssccatid  50179  resccatlem  50180