Theorem ovexi 7392

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  Vcvv 3440  (class class class)co 7358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-sn 4581  df-pr 4583  df-uni 4864  df-iota 6448  df-fv 6500  df-ov 7361

This theorem is referenced by:  negex  11378  decex  12611  eulerthlem2  16709  subccatid  17770  funcres2c  17827  ressffth  17864  fuccofval  17886  fuchom  17888  fuccatid  17896  xpccatid  18111  gsumress  18607  prdssgrpd  18658  smndex1mgm  18832  eqgen  19110  quselbas  19113  quseccl0  19114  qus0subgbas  19127  orbsta  19242  sylow2blem1  19549  sylow2blem2  19550  frgpnabllem1  19802  rngqipbas  21250  rngqiprngimf  21252  rngqiprngghm  21254  rngqiprngimf1  21255  rngqiprnglin  21257  rngqiprngim  21259  rngqiprngfulem1  21266  znle  21491  znbas  21498  znzrhval  21501  relt  21570  retos  21573  frlmlbs  21752  lsslindf  21785  lsslinds  21786  uvcendim  21802  subrgmvr  21988  opsrle  22002  subrgascl  22021  evl1fval  22272  evls1vsca  22317  asclply1subcl  22318  matgsum  22381  matmulr  22382  scmatghm  22477  marepvfval  22509  m2cpmmhm  22689  cpm2mfval  22693  cpmadumatpolylem2  22826  cldsubg  24055  nghmfval  24666  pi1bas  24994  dv11cn  25962  quotval  26256  pserdvlem2  26394  ang180lem3  26777  dchrptlem2  27232  usgrexmpllem  29333  usgrexmpl  29336  nbusgrf1o1  29443  crctcshlem3  29892  2pthon3v  30016  konigsberglem5  30331  konigsberg  30332  bloval  30856  dpval  32971  fzo0pmtrlast  33174  rlocbas  33349  rloccring  33352  rloc0g  33353  rloc1r  33354  rlocf1  33355  zringfrac  33635  resssra  33743  qusdimsum  33785  satfv1fvfmla1  35617  2goelgoanfmla1  35618  satefvfmla1  35619  cdleme31snd  40642  c0exALT  42503  prjcrvfval  42870  prjcrvval  42871  mnringmulrd  44460  subsalsal  46599  isubgr3stgrlem2  48209  isubgr3stgrlem3  48210  isubgr3stgrlem5  48212  usgrexmpl1  48264  usgrexmpl1vtx  48265  usgrexmpl1edg  48266  usgrexmpl2  48269  usgrexmpl2vtx  48270  usgrexmpl2edg  48271  gpgvtx  48285  gpgiedg  48286  naryfvalixp  48871  naryfvalelfv  48874  rrxline  48976  inlinecirc02p  49029  inlinecirc02preu  49030  ssccatid  49313  resccatlem  49314