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 2856	1 ⊢ 𝐴 ∈ V

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  Vcvv 3450  (class class class)co 7415

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 2147  ax-9 2155  ax-ext 2732  ax-nul 5263

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 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-sn 4585  df-pr 4587  df-uni 4868  df-iota 6490  df-fv 6542  df-ov 7418

This theorem is used by:  negex  11501  decex  12762  eulerthlem2  16895  subccatid  17957  funcres2c  18014  ressffth  18051  fuccofval  18073  fuchom  18075  fuccatid  18083  xpccatid  18298  gsumress  18807  prdssgrpd  18858  smndex1mgm  19042  eqgen  19329  quselbas  19335  quseccl0  19336  qus0subgbas  19349  orbsta  19463  sylow2blem1  19770  sylow2blem2  19771  frgpnabllem1  20023  rngqipbas  21527  rngqiprngimf  21529  rngqiprngghm  21531  rngqiprngimf1  21532  rngqiprnglin  21534  rngqiprngim  21536  rngqiprngfulem1  21543  znle  21778  znbas  21785  znzrhval  21788  relt  21857  retos  21860  frlmlbs  22039  lsslindf  22072  lsslinds  22073  uvcendim  22089  subrgmvr  22278  opsrle  22292  subrgascl  22311  evl1fval  22582  evls1vsca  22627  asclply1subcl  22628  matgsum  22688  matmulr  22689  scmatghm  22784  marepvfval  22816  m2cpmmhm  22999  cpm2mfval  23003  cpmadumatpolylem2  23136  cldsubg  24366  nghmfval  24977  pi1bas  25295  dv11cn  26257  quotval  26551  pserdvlem2  26693  ang180lem3  27077  dchrptlem2  27530  usgrexmpllem  29749  usgrexmpl  29752  nbusgrf1o1  29859  crctcshlem3  30316  2pthon3v  30440  konigsberglem5  30765  konigsberg  30766  bloval  31291  dpval  33364  fzo0pmtrlast  33561  rlocbas  33737  rloccring  33740  rloc0g  33741  rloc1r  33742  rlocf1  33743  rlocinvunit  33744  rlocisunit  33745  zringfrac  33994  resssra  34127  qusdimsum  34168  satfv1fvfmla1  36032  2goelgoanfmla1  36033  satefvfmla1  36034  cdleme31snd  41273  c0exALT  43133  prjcrvfval  43491  prjcrvval  43492  mnringmulrd  45075  subsalsal  47201  indprmfz  48547  isubgr3stgrlem2  48897  isubgr3stgrlem3  48898  isubgr3stgrlem5  48900  usgrexmpl1  48952  usgrexmpl1vtx  48953  usgrexmpl1edg  48954  usgrexmpl2  48957  usgrexmpl2vtx  48958  usgrexmpl2edg  48959  gpgvtx  48973  gpgiedg  48974  naryfvalixp  49573  naryfvalelfv  49576  rrxline  49678  inlinecirc02p  49731  inlinecirc02preu  49732  ssccatid  50012  resccatlem  50013