Theorem ovexi 7192

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

Syntax hints:   = wceq 1537   ∈ wcel 2114  Vcvv 3496  (class class class)co 7158

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-nul 5212

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-sn 4570  df-pr 4572  df-uni 4841  df-iota 6316  df-fv 6365  df-ov 7161

This theorem is referenced by:  negex  10886  decex  12105  cshwsexa  14188  eulerthlem2  16121  subccatid  17118  funcres2c  17173  ressffth  17210  fuccofval  17231  fuchom  17233  fuccatid  17241  xpccatid  17440  gsumress  17894  smndex1mgm  18074  eqgen  18335  orbsta  18445  sylow2blem1  18747  sylow2blem2  18748  frgpnabllem1  18995  subrgmvr  20244  opsrle  20258  subrgascl  20280  evl1fval  20493  znle  20685  znbas  20692  znzrhval  20695  relt  20761  retos  20764  frlmlbs  20943  lsslindf  20976  lsslinds  20977  uvcendim  20993  matgsum  21048  matmulr  21049  scmatghm  21144  marepvfval  21176  m2cpmmhm  21355  cpm2mfval  21359  cpmadumatpolylem2  21492  cldsubg  22721  nghmfval  23333  pi1bas  23644  dv11cn  24600  quotval  24883  pserdvlem2  25018  ang180lem3  25391  dchrptlem2  25843  usgrexmpllem  27044  nbusgrf1o1  27154  crctcshlem3  27599  2pthon3v  27724  konigsberglem5  28037  konigsberg  28038  bloval  28560  dpval  30568  qusdimsum  31026  satfv1fvfmla1  32672  2goelgoanfmla1  32673  satefvfmla1  32674  cdleme31snd  37524  c0exALT  39159  subsalsal  42649  rrxline  44728  inlinecirc02p  44781  inlinecirc02preu  44782