MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovexi Structured version   Visualization version   GIF version

Theorem ovexi 7172
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
StepHypRef Expression
1 ovexi.1 . 2 𝐴 = (𝐵𝐹𝐶)
2 ovex 7171 . 2 (𝐵𝐹𝐶) ∈ V
31, 2eqeltri 2912 1 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wcel 2115  Vcvv 3479  (class class class)co 7138
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-nul 5191
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3137  df-rex 3138  df-v 3481  df-sbc 3758  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-sn 4549  df-pr 4551  df-uni 4820  df-iota 6295  df-fv 6344  df-ov 7141
This theorem is referenced by:  negex  10869  decex  12088  cshwsexa  14175  eulerthlem2  16106  subccatid  17105  funcres2c  17160  ressffth  17197  fuccofval  17218  fuchom  17220  fuccatid  17228  xpccatid  17427  gsumress  17881  smndex1mgm  18061  eqgen  18322  orbsta  18432  sylow2blem1  18734  sylow2blem2  18735  frgpnabllem1  18982  subrgmvr  20228  opsrle  20242  subrgascl  20264  evl1fval  20477  znle  20669  znbas  20676  znzrhval  20679  relt  20745  retos  20748  frlmlbs  20927  lsslindf  20960  lsslinds  20961  uvcendim  20977  matgsum  21032  matmulr  21033  scmatghm  21128  marepvfval  21160  m2cpmmhm  21339  cpm2mfval  21343  cpmadumatpolylem2  21476  cldsubg  22705  nghmfval  23317  pi1bas  23632  dv11cn  24593  quotval  24877  pserdvlem2  25012  ang180lem3  25386  dchrptlem2  25838  usgrexmpllem  27039  nbusgrf1o1  27149  crctcshlem3  27594  2pthon3v  27718  konigsberglem5  28030  konigsberg  28031  bloval  28553  dpval  30563  qusdimsum  31045  satfv1fvfmla1  32688  2goelgoanfmla1  32689  satefvfmla1  32690  cdleme31snd  37582  c0exALT  39311  mnringmulrd  40767  subsalsal  42841  naryfvalixp  44884  naryfvalelfv  44887  rrxline  44978  inlinecirc02p  45031  inlinecirc02preu  45032
  Copyright terms: Public domain W3C validator