Theorem ovexi 7445

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

Syntax hints:   = wceq 1567   ∈ wcel 2149  Vcvv 3463  (class class class)co 7411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-nul 5271

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-sn 4595  df-pr 4597  df-uni 4877  df-iota 6493  df-fv 6545  df-ov 7414

This theorem is referenced by:  negex  11455  decex  12715  eulerthlem2  16841  subccatid  17903  funcres2c  17960  ressffth  17997  fuccofval  18019  fuchom  18021  fuccatid  18029  xpccatid  18244  gsumress  18740  prdssgrpd  18791  smndex1mgm  18969  eqgen  19249  quselbas  19255  quseccl0  19256  qus0subgbas  19269  orbsta  19383  sylow2blem1  19690  sylow2blem2  19691  frgpnabllem1  19943  rngqipbas  21406  rngqiprngimf  21408  rngqiprngghm  21410  rngqiprngimf1  21411  rngqiprnglin  21413  rngqiprngim  21415  rngqiprngfulem1  21422  znle  21655  znbas  21662  znzrhval  21665  relt  21734  retos  21737  frlmlbs  21916  lsslindf  21949  lsslinds  21950  uvcendim  21966  subrgmvr  22153  opsrle  22167  subrgascl  22186  evl1fval  22457  evls1vsca  22502  asclply1subcl  22503  matgsum  22563  matmulr  22564  scmatghm  22659  marepvfval  22691  m2cpmmhm  22871  cpm2mfval  22875  cpmadumatpolylem2  23008  cldsubg  24237  nghmfval  24848  pi1bas  25166  dv11cn  26129  quotval  26422  pserdvlem2  26557  ang180lem3  26942  dchrptlem2  27395  usgrexmpllem  29551  usgrexmpl  29554  nbusgrf1o1  29661  crctcshlem3  30109  2pthon3v  30233  konigsberglem5  30548  konigsberg  30549  bloval  31074  dpval  33150  fzo0pmtrlast  33353  rlocbas  33529  rloccring  33532  rloc0g  33533  rloc1r  33534  rlocf1  33535  rlocinvunit  33536  rlocisunit  33537  zringfrac  33789  resssra  33922  qusdimsum  33963  satfv1fvfmla1  35848  2goelgoanfmla1  35849  satefvfmla1  35850  cdleme31snd  41084  c0exALT  42944  prjcrvfval  43289  prjcrvval  43290  mnringmulrd  44873  subsalsal  46999  indprmfz  48305  isubgr3stgrlem2  48655  isubgr3stgrlem3  48656  isubgr3stgrlem5  48658  usgrexmpl1  48710  usgrexmpl1vtx  48711  usgrexmpl1edg  48712  usgrexmpl2  48715  usgrexmpl2vtx  48716  usgrexmpl2edg  48717  gpgvtx  48731  gpgiedg  48732  naryfvalixp  49328  naryfvalelfv  49331  rrxline  49433  inlinecirc02p  49486  inlinecirc02preu  49487  ssccatid  49769  resccatlem  49770