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 483	. 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 396   = wceq 1547   ∈ wcel 2119  Vcvv 3431  ∅c0 4261  dom cdm 5618  Rel wrel 5623  (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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-xp 5624  df-rel 5625  df-dm 5628  df-iota 6441  df-fv 6493  df-ov 7359

This theorem is referenced by:  elfvov1  7398  mapssfset  8788  mapdom2  9076  relexpsucrd  14986  relexpsucld  14987  relexpreld  14993  relexpdmd  14997  relexprnd  15001  relexpfldd  15003  relexpaddd  15007  dfrtrclrec2  15011  relexpindlem  15016  oveqprc  17153  ressinbas  17206  ressress  17208  oduval  18245  oduleval  18246  gsum0  18643  efmndbas  18830  oppgval  19313  oppgplusfval  19314  mgpval  20115  opprval  20309  srasca  21170  rlmsca2  21189  dsmmval  21709  dsmmfi  21713  resspsrbas  21948  mpfrcl  22061  psrbaspropd  22219  mplbaspropd  22221  evl1fval1  22317  qtopres  23681  fgabs  23862  tngds  24631  tcphval  25203  of0r  32771  erlval  33339  fracval  33388  resvsca  33415  mapco2g  43163  mzpmfp  43196  mendbas  43625  naryfvalixp  49120  1aryenef  49136  2aryenef  49147  resccat  49564