Theorem ovprc1 6227

Description: The value of an operation when the first argument is a proper class. (Contributed by NM, 16-Jun-2004.)

Hypothesis

Ref	Expression
ovprc1.1	|- Rel dom F

Assertion

Ref	Expression
ovprc1	|- ( -. A e. _V -> ( A F B ) = (/) )

Proof of Theorem ovprc1

Step	Hyp	Ref	Expression
1		simpl 455	. . 3 |- ( ( A e. _V /\ B e. _V ) -> A e. _V )
2	1	con3i 135	. 2 |- ( -. A e. _V -> -. ( A e. _V /\ B e. _V ) )
3		ovprc1.1	. . 3 |- Rel dom F
4	3	ovprc 6226	. 2 |- ( -. ( A e. _V /\ B e. _V ) -> ( A F B ) = (/) )
5	2, 4	syl 16	1 |- ( -. A e. _V -> ( A F B ) = (/) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 367   = wceq 1399   e. wcel 1826   _Vcvv 3034   (/)c0 3711   dom cdm 4913   Rel wrel 4918  (class class class)co 6196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-xp 4919  df-rel 4920  df-dm 4923  df-iota 5460  df-fv 5504  df-ov 6199

This theorem is referenced by:  mapdom2  7607  setsnid  14678  ressbas  14691  resslem  14694  ressinbas  14697  ressress  14699  oduval  15877  oduleval  15878  gsum0  16022  oppgval  16499  oppgplusfval  16500  mgpval  17257  opprval  17386  srasca  17940  rlmsca2  17960  resspsrbas  18183  mpfrcl  18300  psrbaspropd  18389  mplbaspropd  18391  evl1fval1  18480  dsmmval  18856  dsmmbas2  18859  dsmmfi  18860  qtopres  20284  fgabs  20465  tnglem  21239  tngds  21247  tchval  21746  resvsca  27974  resvlem  27975  mapco2g  30812  mzpmfp  30845  mendbas  31301