Theorem ovexi 7444

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2143  Vcvv 3455  (class class class)co 7410

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5269

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-sn 4590  df-pr 4592  df-uni 4873  df-iota 6492  df-fv 6544  df-ov 7413

This theorem is used by:  negex  11459  decex  12719  eulerthlem2  16845  subccatid  17907  funcres2c  17964  ressffth  18001  fuccofval  18023  fuchom  18025  fuccatid  18033  xpccatid  18248  gsumress  18744  prdssgrpd  18795  smndex1mgm  18973  eqgen  19253  quselbas  19259  quseccl0  19260  qus0subgbas  19273  orbsta  19387  sylow2blem1  19694  sylow2blem2  19695  frgpnabllem1  19947  rngqipbas  21444  rngqiprngimf  21446  rngqiprngghm  21448  rngqiprngimf1  21449  rngqiprnglin  21451  rngqiprngim  21453  rngqiprngfulem1  21460  znle  21695  znbas  21702  znzrhval  21705  relt  21774  retos  21777  frlmlbs  21956  lsslindf  21989  lsslinds  21990  uvcendim  22006  subrgmvr  22193  opsrle  22207  subrgascl  22226  evl1fval  22497  evls1vsca  22542  asclply1subcl  22543  matgsum  22603  matmulr  22604  scmatghm  22699  marepvfval  22731  m2cpmmhm  22911  cpm2mfval  22915  cpmadumatpolylem2  23048  cldsubg  24277  nghmfval  24888  pi1bas  25206  dv11cn  26169  quotval  26462  pserdvlem2  26600  ang180lem3  26985  dchrptlem2  27438  usgrexmpllem  29619  usgrexmpl  29622  nbusgrf1o1  29729  crctcshlem3  30177  2pthon3v  30301  konigsberglem5  30616  konigsberg  30617  bloval  31142  dpval  33218  fzo0pmtrlast  33421  rlocbas  33597  rloccring  33600  rloc0g  33601  rloc1r  33602  rlocf1  33603  rlocinvunit  33604  rlocisunit  33605  zringfrac  33853  resssra  33986  qusdimsum  34027  satfv1fvfmla1  35923  2goelgoanfmla1  35924  satefvfmla1  35925  cdleme31snd  41188  c0exALT  43048  prjcrvfval  43391  prjcrvval  43392  mnringmulrd  44975  subsalsal  47101  indprmfz  48410  isubgr3stgrlem2  48760  isubgr3stgrlem3  48761  isubgr3stgrlem5  48763  usgrexmpl1  48815  usgrexmpl1vtx  48816  usgrexmpl1edg  48817  usgrexmpl2  48820  usgrexmpl2vtx  48821  usgrexmpl2edg  48822  gpgvtx  48836  gpgiedg  48837  naryfvalixp  49437  naryfvalelfv  49440  rrxline  49542  inlinecirc02p  49595  inlinecirc02preu  49596  ssccatid  49878  resccatlem  49879