Theorem ovprc1 7429

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 7428	. 2 ⊢ (¬ (𝐴 ∈ V ∧ 𝐵 ∈ V) → (𝐴𝐹𝐵) = ∅)
4	1, 3	nsyl5 159	1 ⊢ (¬ 𝐴 ∈ V → (𝐴𝐹𝐵) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3450  ∅c0 4299  dom cdm 5641  Rel wrel 5646  (class class class)co 7390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-dm 5651  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  elfvov1  7432  mapssfset  8827  mapdom2  9118  relexpsucrd  15006  relexpsucld  15007  relexpreld  15013  relexpdmd  15017  relexprnd  15021  relexpfldd  15023  relexpaddd  15027  dfrtrclrec2  15031  relexpindlem  15036  oveqprc  17169  ressinbas  17222  ressress  17224  oduval  18256  oduleval  18257  gsum0  18618  efmndbas  18805  oppgval  19286  oppgplusfval  19287  mgpval  20059  opprval  20254  srasca  21094  rlmsca2  21113  dsmmval  21650  dsmmfi  21654  resspsrbas  21890  mpfrcl  21999  psrbaspropd  22126  mplbaspropd  22128  evl1fval1  22225  qtopres  23592  fgabs  23773  tngds  24543  tcphval  25125  of0r  32609  erlval  33216  fracval  33261  resvsca  33311  mapco2g  42709  mzpmfp  42742  mendbas  43176  naryfvalixp  48622  1aryenef  48638  2aryenef  48649  resccat  49067