Theorem ovexi 7449

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

Syntax hints:   = wceq 1534   ∈ wcel 2099  Vcvv 3470  (class class class)co 7415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-nul 5301

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2937  df-v 3472  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-sn 4626  df-pr 4628  df-uni 4905  df-iota 6495  df-fv 6551  df-ov 7418

This theorem is referenced by:  negex  11483  decex  12706  cshwsexaOLD  14802  eulerthlem2  16745  subccatid  17826  funcres2c  17884  ressffth  17921  fuccofval  17944  fuchom  17946  fuchomOLD  17947  fuccatid  17955  xpccatid  18173  gsumress  18636  prdssgrpd  18687  smndex1mgm  18853  eqgen  19130  quselbas  19133  quseccl0  19134  qus0subgbas  19147  orbsta  19258  sylow2blem1  19569  sylow2blem2  19570  frgpnabllem1  19822  rngqipbas  21179  rngqiprngimf  21181  rngqiprngghm  21183  rngqiprngimf1  21184  rngqiprnglin  21186  rngqiprngim  21188  rngqiprngfulem1  21195  znle  21460  znbas  21471  znzrhval  21474  relt  21541  retos  21544  frlmlbs  21725  lsslindf  21758  lsslinds  21759  uvcendim  21775  subrgmvr  21965  opsrle  21979  subrgascl  22004  evl1fval  22241  matgsum  22333  matmulr  22334  scmatghm  22429  marepvfval  22461  m2cpmmhm  22641  cpm2mfval  22645  cpmadumatpolylem2  22778  cldsubg  24009  nghmfval  24633  pi1bas  24959  dv11cn  25928  quotval  26221  pserdvlem2  26359  ang180lem3  26737  dchrptlem2  27192  usgrexmpllem  29067  nbusgrf1o1  29177  crctcshlem3  29624  2pthon3v  29748  konigsberglem5  30060  konigsberg  30061  bloval  30585  dpval  32608  rlocbas  32976  rloccring  32979  rloc0g  32980  rloc1r  32981  rlocf1  32982  zringfrac  32991  evls1vsca  33246  asclply1subcl  33252  resssra  33278  qusdimsum  33317  satfv1fvfmla1  35028  2goelgoanfmla1  35029  satefvfmla1  35030  cdleme31snd  39854  evlsvvvallem2  41786  evlsvvval  41787  evlsmhpvvval  41819  mhphf  41821  c0exALT  41825  prjcrvfval  42046  prjcrvval  42047  mnringmulrd  43649  subsalsal  45738  naryfvalixp  47693  naryfvalelfv  47696  rrxline  47798  inlinecirc02p  47851  inlinecirc02preu  47852