NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ovex GIF version

Theorem ovex 5551
Description: The result of an operation is a set. (Contributed by set.mm contributors, 13-Mar-1995.)
Assertion
Ref Expression
ovex (AFB) V

Proof of Theorem ovex
StepHypRef Expression
1 df-ov 5526 . 2 (AFB) = (FA, B)
2 fvex 5339 . 2 (FA, B) V
31, 2eqeltri 2423 1 (AFB) V
Colors of variables: wff setvar class
Syntax hints:   wcel 1710  Vcvv 2859  cop 4561  cfv 4781  (class class class)co 5525
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-ss 3259  df-nul 3551  df-sn 3741  df-pr 3742  df-uni 3892  df-iota 4339  df-fv 4795  df-ov 5526
This theorem is referenced by:  ovelrn  5608  ndmovass  5618  ndmovdistr  5619  caov4  5639  caov411  5640  caovdir  5642  caovdilem  5643  caovlem2  5644  enmap2lem1  6063  enmap1lem1  6069  enprmaplem1  6076  ovcelem1  6171  ceex  6174  ce0nnul  6177  ce0nnulb  6182  ceclb  6183  fce  6188  ce0  6190  ce2  6192  ncvsq  6256  spaccl  6286  spacind  6287  spacis  6288  nchoicelem9  6297
  Copyright terms: Public domain W3C validator