Theorem ovexi 7453

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2146  Vcvv 3457  (class class class)co 7419

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 2148  ax-9 2156  ax-ext 2737  ax-nul 5271

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 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-sn 4592  df-pr 4594  df-uni 4875  df-iota 6496  df-fv 6548  df-ov 7422

This theorem is used by:  negex  11474  decex  12735  eulerthlem2  16867  subccatid  17929  funcres2c  17986  ressffth  18023  fuccofval  18045  fuchom  18047  fuccatid  18055  xpccatid  18270  gsumress  18776  prdssgrpd  18827  smndex1mgm  19010  eqgen  19297  quselbas  19303  quseccl0  19304  qus0subgbas  19317  orbsta  19431  sylow2blem1  19738  sylow2blem2  19739  frgpnabllem1  19991  rngqipbas  21489  rngqiprngimf  21491  rngqiprngghm  21493  rngqiprngimf1  21494  rngqiprnglin  21496  rngqiprngim  21498  rngqiprngfulem1  21505  znle  21740  znbas  21747  znzrhval  21750  relt  21819  retos  21822  frlmlbs  22001  lsslindf  22034  lsslinds  22035  uvcendim  22051  subrgmvr  22238  opsrle  22252  subrgascl  22271  evl1fval  22542  evls1vsca  22587  asclply1subcl  22588  matgsum  22648  matmulr  22649  scmatghm  22744  marepvfval  22776  m2cpmmhm  22956  cpm2mfval  22960  cpmadumatpolylem2  23093  cldsubg  24323  nghmfval  24934  pi1bas  25252  dv11cn  26215  quotval  26508  pserdvlem2  26646  ang180lem3  27031  dchrptlem2  27484  usgrexmpllem  29672  usgrexmpl  29675  nbusgrf1o1  29782  crctcshlem3  30239  2pthon3v  30363  konigsberglem5  30682  konigsberg  30683  bloval  31208  dpval  33283  fzo0pmtrlast  33480  rlocbas  33656  rloccring  33659  rloc0g  33660  rloc1r  33661  rlocf1  33662  rlocinvunit  33663  rlocisunit  33664  zringfrac  33912  resssra  34045  qusdimsum  34086  satfv1fvfmla1  35956  2goelgoanfmla1  35957  satefvfmla1  35958  cdleme31snd  41222  c0exALT  43082  prjcrvfval  43440  prjcrvval  43441  mnringmulrd  45024  subsalsal  47150  indprmfz  48459  isubgr3stgrlem2  48809  isubgr3stgrlem3  48810  isubgr3stgrlem5  48812  usgrexmpl1  48864  usgrexmpl1vtx  48865  usgrexmpl1edg  48866  usgrexmpl2  48869  usgrexmpl2vtx  48870  usgrexmpl2edg  48871  gpgvtx  48885  gpgiedg  48886  naryfvalixp  49485  naryfvalelfv  49488  rrxline  49590  inlinecirc02p  49643  inlinecirc02preu  49644  ssccatid  49926  resccatlem  49927