Theorem ovprc1 7395

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 𝐹

Assertion

Ref	Expression
ovprc1	⊢ (¬ 𝐴 ∈ V → (𝐴𝐹𝐵) = ∅)

Proof of Theorem ovprc1

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → 𝐴 ∈ V)
2		ovprc1.1	. . 3 ⊢ Rel dom 𝐹
3	2	ovprc 7394	. 2 ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐹𝐵) = ∅)
4	1, 3	nsyl5 159	1 ⊢ (¬ 𝐴 ∈ V → (𝐴𝐹𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  Vcvv 3438  ∅c0 4283  dom cdm 5622  Rel wrel 5627  (class class class)co 7356

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-xp 5628  df-rel 5629  df-dm 5632  df-iota 6446  df-fv 6498  df-ov 7359

This theorem is referenced by:  elfvov1  7398  mapssfset  8786  mapdom2  9074  relexpsucrd  14954  relexpsucld  14955  relexpreld  14961  relexpdmd  14965  relexprnd  14969  relexpfldd  14971  relexpaddd  14975  dfrtrclrec2  14979  relexpindlem  14984  oveqprc  17117  ressinbas  17170  ressress  17172  oduval  18209  oduleval  18210  gsum0  18607  efmndbas  18794  oppgval  19274  oppgplusfval  19275  mgpval  20076  opprval  20272  srasca  21130  rlmsca2  21149  dsmmval  21687  dsmmfi  21691  resspsrbas  21927  mpfrcl  22038  psrbaspropd  22173  mplbaspropd  22175  evl1fval1  22273  qtopres  23640  fgabs  23821  tngds  24590  tcphval  25172  of0r  32707  erlval  33289  fracval  33335  resvsca  33362  mapco2g  42898  mzpmfp  42931  mendbas  43364  naryfvalixp  48817  1aryenef  48833  2aryenef  48844  resccat  49261