Theorem ovexi 7447

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

Syntax hints:   = wceq 1539   ∈ wcel 2104  Vcvv 3472  (class class class)co 7413

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-nul 5307

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-sn 4630  df-pr 4632  df-uni 4910  df-iota 6496  df-fv 6552  df-ov 7416

This theorem is referenced by:  negex  11464  decex  12687  cshwsexaOLD  14781  eulerthlem2  16721  subccatid  17802  funcres2c  17858  ressffth  17895  fuccofval  17917  fuchom  17919  fuchomOLD  17920  fuccatid  17928  xpccatid  18146  gsumress  18609  prdssgrpd  18660  smndex1mgm  18826  eqgen  19099  quselbas  19101  quseccl0  19102  qus0subgbas  19115  orbsta  19220  sylow2blem1  19531  sylow2blem2  19532  frgpnabllem1  19784  rngqipbas  21056  rngqiprngimf  21058  rngqiprngghm  21060  rngqiprngimf1  21061  rngqiprnglin  21063  rngqiprngim  21065  rngqiprngfulem1  21072  znle  21309  znbas  21320  znzrhval  21323  relt  21389  retos  21392  frlmlbs  21573  lsslindf  21606  lsslinds  21607  uvcendim  21623  subrgmvr  21809  opsrle  21823  subrgascl  21848  evl1fval  22069  matgsum  22161  matmulr  22162  scmatghm  22257  marepvfval  22289  m2cpmmhm  22469  cpm2mfval  22473  cpmadumatpolylem2  22606  cldsubg  23837  nghmfval  24461  pi1bas  24787  dv11cn  25752  quotval  26039  pserdvlem2  26174  ang180lem3  26550  dchrptlem2  27002  usgrexmpllem  28782  nbusgrf1o1  28892  crctcshlem3  29338  2pthon3v  29462  konigsberglem5  29774  konigsberg  29775  bloval  30299  dpval  32321  evls1vsca  32922  asclply1subcl  32932  resssra  32960  qusdimsum  32999  satfv1fvfmla1  34710  2goelgoanfmla1  34711  satefvfmla1  34712  cdleme31snd  39562  evlsvvvallem2  41438  evlsvvval  41439  evlsmhpvvval  41471  mhphf  41473  c0exALT  41477  prjcrvfval  41677  prjcrvval  41678  mnringmulrd  43284  subsalsal  45375  naryfvalixp  47404  naryfvalelfv  47407  rrxline  47509  inlinecirc02p  47562  inlinecirc02preu  47563