Theorem ovexi 7380

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

Syntax hints:   = wceq 1541   ∈ wcel 2111  Vcvv 3436  (class class class)co 7346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5242

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-sn 4574  df-pr 4576  df-uni 4857  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  negex  11358  decex  12592  eulerthlem2  16693  subccatid  17753  funcres2c  17810  ressffth  17847  fuccofval  17869  fuchom  17871  fuccatid  17879  xpccatid  18094  gsumress  18590  prdssgrpd  18641  smndex1mgm  18815  eqgen  19093  quselbas  19096  quseccl0  19097  qus0subgbas  19110  orbsta  19225  sylow2blem1  19532  sylow2blem2  19533  frgpnabllem1  19785  rngqipbas  21232  rngqiprngimf  21234  rngqiprngghm  21236  rngqiprngimf1  21237  rngqiprnglin  21239  rngqiprngim  21241  rngqiprngfulem1  21248  znle  21473  znbas  21480  znzrhval  21483  relt  21552  retos  21555  frlmlbs  21734  lsslindf  21767  lsslinds  21768  uvcendim  21784  subrgmvr  21968  opsrle  21982  subrgascl  22001  evl1fval  22243  evls1vsca  22288  asclply1subcl  22289  matgsum  22352  matmulr  22353  scmatghm  22448  marepvfval  22480  m2cpmmhm  22660  cpm2mfval  22664  cpmadumatpolylem2  22797  cldsubg  24026  nghmfval  24637  pi1bas  24965  dv11cn  25933  quotval  26227  pserdvlem2  26365  ang180lem3  26748  dchrptlem2  27203  usgrexmpllem  29238  usgrexmpl  29241  nbusgrf1o1  29348  crctcshlem3  29797  2pthon3v  29921  konigsberglem5  30236  konigsberg  30237  bloval  30761  dpval  32870  fzo0pmtrlast  33061  rlocbas  33234  rloccring  33237  rloc0g  33238  rloc1r  33239  rlocf1  33240  zringfrac  33519  resssra  33599  qusdimsum  33641  satfv1fvfmla1  35467  2goelgoanfmla1  35468  satefvfmla1  35469  cdleme31snd  40495  c0exALT  42355  prjcrvfval  42734  prjcrvval  42735  mnringmulrd  44326  subsalsal  46467  isubgr3stgrlem2  48077  isubgr3stgrlem3  48078  isubgr3stgrlem5  48080  usgrexmpl1  48132  usgrexmpl1vtx  48133  usgrexmpl1edg  48134  usgrexmpl2  48137  usgrexmpl2vtx  48138  usgrexmpl2edg  48139  gpgvtx  48153  gpgiedg  48154  naryfvalixp  48740  naryfvalelfv  48743  rrxline  48845  inlinecirc02p  48898  inlinecirc02preu  48899  ssccatid  49183  resccatlem  49184