Theorem ovexi 7464

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2146  Vcvv 3454  (class class class)co 7430

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-nul 5263

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-sn 4589  df-pr 4591  df-uni 4871  df-iota 6501  df-fv 6555  df-ov 7433

This theorem is used by:  negex  11568  decex  12831  eulerthlem2  16974  subccatid  18036  funcres2c  18093  ressffth  18130  fuccofval  18152  fuchom  18154  fuccatid  18162  xpccatid  18377  gsumress  18886  prdssgrpd  18937  smndex1mgm  19121  eqgen  19408  quselbas  19414  quseccl0  19415  qus0subgbas  19428  orbsta  19542  sylow2blem1  19849  sylow2blem2  19850  frgpnabllem1  20102  rngqipbas  21606  rngqiprngimf  21608  rngqiprngghm  21610  rngqiprngimf1  21611  rngqiprnglin  21613  rngqiprngim  21615  rngqiprngfulem1  21622  znle  21857  znbas  21864  znzrhval  21867  relt  21936  retos  21939  frlmlbs  22118  lsslindf  22151  lsslinds  22152  uvcendim  22168  subrgmvr  22357  opsrle  22371  subrgascl  22390  evl1fval  22661  evls1vsca  22706  asclply1subcl  22707  matgsum  22767  matmulr  22768  scmatghm  22863  marepvfval  22895  m2cpmmhm  23078  cpm2mfval  23082  cpmadumatpolylem2  23215  cldsubg  24445  nghmfval  25056  pi1bas  25374  dv11cn  26336  quotval  26628  pserdvlem2  26770  ang180lem3  27154  dchrptlem2  27607  usgrexmpllem  29856  usgrexmpl  29859  nbusgrf1o1  29966  crctcshlem3  30423  2pthon3v  30547  konigsberglem5  30872  konigsberg  30873  bloval  31398  dpval  33512  fzo0pmtrlast  33709  rlocbas  33885  rloccring  33888  rloc0g  33889  rloc1r  33890  rlocf1  33891  rlocinvunit  33892  rlocisunit  33893  zringfrac  34142  resssra  34275  qusdimsum  34316  satfv1fvfmla1  36312  2goelgoanfmla1  36313  satefvfmla1  36314  cdleme31snd  41589  c0exALT  43449  prjcrvfval  43813  prjcrvval  43814  mnringmulrd  45367  subsalsal  47514  indprmfz  48860  isubgr3stgrlem2  49210  isubgr3stgrlem3  49211  isubgr3stgrlem5  49213  usgrexmpl1  49265  usgrexmpl1vtx  49266  usgrexmpl1edg  49267  usgrexmpl2  49270  usgrexmpl2vtx  49271  usgrexmpl2edg  49272  gpgvtx  49286  gpgiedg  49287  naryfvalixp  49886  naryfvalelfv  49889  rrxline  49992  2sphere0  50007  line2x  50011  line2y  50012  inlinecirc02p  50044  inlinecirc02preu  50045  ssccatid  50331  resccatlem  50332